TY - GEN

T1 - A logically saturated extension of λ¯μμ~

AU - Mamane, Lionel Elie

AU - Geuvers, Herman

AU - McKinna, James

PY - 2009

Y1 - 2009

N2 - This paper presents a proof language based on the work of Sacerdoti Coen [1,2], Kirchner [3] and Autexier [4] on ̄μμ̃, a calculus introduced by Curien and Herbelin. [5,6] Just as ̄μμ̃ preserves several proof structures that are identified by the λ-calculus, the proof language presented here aims to preserve as much proof structure as reasonable; we call that property being logically saturated. This leads to several advantages when the language is used as a generic exchange language for proofs, as well as for other uses. We equip the calculus with a simple rendering in pseudo-natural language that aims to give people tools to read, understand and exchange terms of the language. We show how this rendering can, at the cost of some more complexity, be made to produce text that is more natural and idiomatic, or in the style of a declarative proof language like Isar or Mizar.

AB - This paper presents a proof language based on the work of Sacerdoti Coen [1,2], Kirchner [3] and Autexier [4] on ̄μμ̃, a calculus introduced by Curien and Herbelin. [5,6] Just as ̄μμ̃ preserves several proof structures that are identified by the λ-calculus, the proof language presented here aims to preserve as much proof structure as reasonable; we call that property being logically saturated. This leads to several advantages when the language is used as a generic exchange language for proofs, as well as for other uses. We equip the calculus with a simple rendering in pseudo-natural language that aims to give people tools to read, understand and exchange terms of the language. We show how this rendering can, at the cost of some more complexity, be made to produce text that is more natural and idiomatic, or in the style of a declarative proof language like Isar or Mizar.

UR - http://www.scopus.com/inward/record.url?scp=69049092800&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-02614-0_32

DO - 10.1007/978-3-642-02614-0_32

M3 - Conference contribution

AN - SCOPUS:69049092800

SN - 3642026133

SN - 9783642026133

T3 - Lecture Notes in Computer Science

SP - 405

EP - 421

BT - Intelligent Computer Mathematics. CICM 2009

PB - Springer

ER -