ALF 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 all top 5 Cited in 13 Serials 5 Information and Computation 4 Theoretical Computer Science 3 Journal of Functional Programming 2 Annals of Pure and Applied Logic 2 Journal of Automated Reasoning 2 Journal of Logic and Computation 2 The Journal of Logic and Algebraic Programming 1 MSCS. Mathematical Structures in Computer Science 1 Indagationes Mathematicae. New Series 1 Higher-Order and Symbolic Computation 1 Sādhanā 1 ACM Transactions on Computational Logic 1 Journal of Applied Logic all top 5 Cited in 7 Fields 57 Computer science (68-XX) 41 Mathematical logic and foundations (03-XX) 3 Geometry (51-XX) 1 General and overarching topics; collections (00-XX) 1 Category theory; homological algebra (18-XX) 1 Manifolds and cell complexes (57-XX) 1 Numerical analysis (65-XX) Citations by Year