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 52 articles )
Showing results 1 to 20 of 52.
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)
- Ranta, Aarne: Translating between language and logic: what is easy and what is difficult (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)
- Nanevski, Aleksandar; Pfenning, Frank; Pientka, Brigitte: Contextual modal type theory (2008)
- Asperti, Andrea; Sacerdoti Coen, Claudio; Tassi, Enrico; Zacchiroli, Stefano: Crafting a proof assistant (2007)
- Stump, Aaron: Imperative LF meta-programming (2007)
- Lindblad, Fredrik; Benke, Marcin: A tool for automated theorem proving in Agda (2006)
- Morris, Peter; Altenkirch, Thorsten; McBride, Conor: Exploring the regular tree types (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)
- Kutsia, Temur; Buchberger, Bruno: Predicate logic with sequence variables and sequence function symbols (2004)
- 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)