swMATH ID: 8603
Software Authors: Lena Magnusson
Description: 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. ...
Homepage: http://homepages.inf.ed.ac.uk/wadler/realworld/alf.html
Related Software: Coq; Automath; Nuprl; LEGO; Isabelle; Twelf; HOL; Elf; Agda; Flyspeck; LCF; Cayenne; PVS; OMDoc; Mizar; Isar; Haskell; ML; kepler98; Matita
Cited in: 67 Publications
all top 5

Cited by 77 Authors

5 Pfenning, Frank
3 Callaghan, Paul T.
3 Despeyroux, Joëlle
3 Kamareddine, Fairouz D.
3 Luo, Zhaohui
3 Muñoz, César A.
3 Ranta, Aarne
3 Schürmann, Carsten
3 Severi, Paula Gabriela
2 Altenkirch, Thorsten
2 Ayala-Rincón, Mauricio
2 Buchberger, Bruno
2 Cederquist, Jan
2 Coquand, Catarina
2 Cavalcanti de Moura, Flávio Leonardo
2 Geuvers, Jan Herman
2 Jojgov, Gueorgui I.
2 Kirchner, Florent
2 Pientka, Brigitte
2 von Plato, Jan
1 Adams, Robin
1 Agerholm, Sten
1 Asperti, Andrea
1 Barendregt, Hendrik Pieter
1 Barthe, Gilles
1 Benke, Marcin
1 Berghofer, Stefan
1 Bertot, Yves
1 Betarte, Gustavo
1 Bove, Ana
1 Calderón, Guillermo
1 Calude, Cristian S.
1 Capretta, Venanzio
1 Cave, Andrew
1 Constable, Robert Lee
1 Cooper, Robin
1 Dehlinger, Christophe
1 Dufourd, Jean-François
1 Duggan, Dominic
1 Dybjer, Peter
1 Felty, Amy P.
1 Gabbay, Murdoch James
1 Gordon, Mike J.
1 Hedberg, Michael
1 Holm, Ruurik
1 Horozal, Fulya
1 Jansson, Patrik
1 Ko, Hsiang-Shang
1 Kutsia, Temur
1 Leleu, Pierre
1 Lindblad, Fredrik
1 Luther, Marko
1 Magaud, Nicolas
1 Magnusson, Lena
1 McBride, Conor Thomas
1 Miculan, Marino
1 Morris, Peter A.
1 Mu, Shin-Cheng
1 Mulligan, Dominic P.
1 Nanevski, Aleksandar
1 Negri, Sara
1 Paulin-Mohring, Christine
1 Pierce, Benjamin C.
1 Rabe, Florian
1 Ríos, Alejandro
1 Ruys, Mark
1 Sacerdoti Coen, Claudio
1 Setzer, Anton
1 Smith, Jan M.
1 Strecker, Martin
1 Stump, Aaron
1 Szasz, Nora
1 Tammet, Tanel
1 Tassi, Enrico
1 Thompson, Declan
1 von Henke, Friedrich Wilhelm
1 Zacchiroli, Stefano

Citations by Year