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 67 articles )
Showing results 1 to 20 of 67.
Sorted by year (- Calderón, Guillermo: Formalizing constructive projective geometry in Agda (2018)
- Calude, Cristian S.; Thompson, Declan: Incompleteness, undecidability and automated proofs (invited talk) (2016)
- 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)
- Gabbay, Murdoch J.; Mulligan, Dominic P.: Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms (2010)
- 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)
- Kirchner, Florent; Muñoz, César: PVS#: streamlined tacticals for PVS (2007)
- Stump, Aaron: Imperative LF meta-programming (2007)
- Dybjer, Peter; Setzer, Anton: Indexed induction-recursion (2006)
- 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)