ALF
The Implementation of ALF - a Proof Editor based on Martin-Löf’s Monomorphic Type Theory with Explicit Substitution. This thesis describes the implementation of ALF, which is an interactive proof editor based on Martin-Löf’s type theory with explicit substitutions. ALF is a general purpose proof assistant, in which different logics can be represented. Proof objects are manipulated directly, by the usual editing operations. A partial proof is represented as an incomplete proof object, i.e., a proof object containing placeholders. A modular type/proof checking algorithm for complete proof objects is presented, and it is proved sound and complete assuming some basic meta theory properties of the substitution calculus. The algorithm is extended to handle incomplete objects in such a way that the type checking problem is reduced to a unication problem, i.e., the problem of finding instantiations to the placeholders in the object. ...
Keywords for this software
References in zbMATH (referenced in 49 articles )
Showing results 1 to 20 of 49.
Sorted by year (- Pientka, Brigitte; Cave, Andrew: Inductive Beluga: programming proofs (2015)
- Ranta, Aarne: Machine translation and type theory (2012)
- Horozal, Fulya; Rabe, Florian: Representing model theory in a type-theoretical logical framework (2011)
- Kirchner, Florent; Muñoz, César: The proof monad (2010)
- Geuvers, H.: Proof assistants: history, ideas and future (2009)
- Mu, Shin-Cheng; Ko, Hsiang-Shang; Jansson, Patrik: Algebra of programming in Agda: dependent types for relational program derivation (2009)
- Stump, Aaron: Imperative LF meta-programming. (2008)
- Asperti, Andrea; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano: Crafting a proof assistant (2007)
- Kirchner, Florent; Muñoz, César: PVS#: Streamlined tacticals for PVS. (2007)
- Stump, Aaron: Imperative LF meta-programming (2007)
- Lindblad, Fredrik; Benke, Marcin: A tool for automated theorem proving in Agda (2006)
- Ayala-Rincón, Mauricio; de Moura, Flávio L.C.; Kamareddine, Fairouz: Comparing and implementing calculi of explicit substitutions with eta-reduction (2005)
- Cooper, Robin: Records and record types in semantic theory (2005)
- Pierce, Benjamin C. (ed.): Advanced topics in types and programming languages. (2005)
- Adams, Robin: A modular hierarchy of logical frameworks (2004)
- Buchberger, Bruno: Algorithm-supported mathematical theory exploration: A personal view and strategy (2004)
- Jojgov, Gueorgui I.: Tactics and parameters. (2003)
- Ayala-Rincón, Mauricio; De Moura, Flávio L.C.; Kamareddine, Fairouz: Comparing calculi of explicit substitutions with eta-reduction (2002)
- Coquand, Catarina: A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions (2002)
- Dehlinger, Christophe; Dufourd, Jean-François: Formalizing the trading theorem for the classification of surfaces (2002)