A Logically Saturated Extension of λ¯μμ~

Lionel Elie Mamane, Herman Geuvers, James Mckinna

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publication16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009. Proceedings
PublisherSpringer Berlin Heidelberg
Pages405-421
Number of pages17
Volume5625
ISBN (Electronic)978-3-642-02614-0
ISBN (Print)978-3-642-02613-3
DOIs
Publication statusPublished - 2009

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume5625
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'A Logically Saturated Extension of λ¯μμ~'. Together they form a unique fingerprint.

Cite this