Experiments in Machine-Checked Proofs

Computing Science Applications

Programming Languages

• Properties of a functional language. Alvaro Tasistro. [ALF] [PS]
• Subject Reduction for a small typed functional language. Ana Bove. [PS]
• Integrated Verification in Type Theory (Thorsten Altenkirch,1996)
• Infinite Objects and Graph Reduction (Catarina Coquand) [PS]
• Lambda-calculus with explicit substitutions. (Catarina Coquand,1993) [PS]
• Alfa-conversion in Simply Typed Lambda Calculus. Ana Bove, Paula Severi [PS]
• Zip function. (Daniel Fridlender, Mia Indrika, 1998) [Agda] [PS] [slides.PS]
• Simple properties of functional programs. (Patrik Jansson, 1999) [Agda]
• Type-checker for simply typed lambda calcucus. (Thierry Coquand, 1994) [ALF]

Algorithms

• Sorting (Thorsten Altenkirch) [ALF] [DVI]
• Integrated version of a sorting algorithm. (Thierry Coquand) [ALF]
• Abstract insertion sort. Alvaro Tasistro. 1995. [DVI]
• Binomial Queues (Björn von Sydow) [PS]
• Linear search, Insertion sort. (Björn von Sydow,1994) [PS]
• Unification. Ana Bove, [PS]

Concurrency

• formalisation of notions from process calculus. (Prasad, Pawel Paczkowski,1994) written in ALF, now is being updated for AGDA
• Bisimulation in CCS (Karlis Cerans, 1993) [DVI]
• Distributed Sorting. (Prasad, Ed Harcourt, Joergen Andersen,1996) [ALF]
• Properties of FCBS (Martin Weichert) [ALF]

Linguistics

• Type Theoretical Grammar. Aarne Ranta. Oxford University Press, 1994
• Grammatical Framework. Aarne Ranta.
• Syntactical categories via type theory. Aarne Ranta [ALF] [PS]

Hardware Verification

• Circuits for natural arithmetic (Magnus Andersson) [ALF] [PS]
• Some concepts of Ruby specification language (Matthias Sauer, Mary Sheeran) [half]

Mathematics

Logic

• a proof that Ackermann's function is not primitive recursive. (Nora Szasz, 1991) [ALF] [PS]
• Cut-elimination for minimal logic. (Thierry Coquand) [ALF]
• Normalisation proof for intuitionistic propositional logic. (Peter Dybjer) [ALF]
• Categorical combinators for dependent types (Peter Dybjer) [ALF]
• Combinatorial completeness of untyped combinators. (Veronica Gaspes, 1992) [ALF] [PS]
• Normalisation proof for simply typed combinators. [ALF] (Veronica Gaspes, 1992) [PS]
• Constructive Completeness of Intuitionistic Predicate Logic. (Henrik Persson, 1996) [ALF] [PS] [Licensiate]
• P. Aczel's CZF (Makoto Takeyama) [Agda]

Algebra

• Systems of Algebras. ( Gustavo Betarte, Alvaro Tasistro, 1995). [ALF] [PS]
• Integers forms an Integral Domain. (Gustavo Betarte, 1993) [ALF] [PS]
• Associativity. (Michael Hedberg, 1991) [ALF]
• Semilattices. (Michael Hedberg) [ALF]
• Polynomial ring. (Henrik Persson, 1997) [Agda] [PS] [Ph.D.]
• Zantema Problem. (Thierry Coquand, Henrik Persson, 1997) [Agda] [PS]
• Gröbner Bases. (Thierry Coquand, Henrik Persson, 1998) [Agda] [PS]

Category Theory

• Category of Sets with Universes (Veronica Gaspes, Peter Dybjer) [ALF] [PS]
• Internal Type Theory (Peter Dybjer) [PS]
• Coherence Theorem for Monoidal Category, Ilya Beylin and Peter Dybjer [ALF] [PS]
• Coherence for Symmetric Monoidal Category. (Ilya Beylin). [AGDA] [PS]
• Path Category. Ilya Beylin. [Agda] [PS]
• Allegory of E-Relations. Carlos Gonzalia, 1999 [Agda] [PS]
• E-Categories, Qiao ) [Agda]
• Formulas-as-Types-as-Objects, Qiao, [Agda] [PS]
• Families to define globular sets. Makoto Takeyama. [Agda]
• Definition of enriched categories. Makoto Takeyama. [Agda]

Formal Topology

• Definitions and applications to domain theory, (Jan Cederquist, 1994) [ALF] [PS]
• Heine-Borel covering lemma, (Jan Cederquist and Sara Negri, 1996) [half] [PS]
• Hahn-Banach theorem (Jan Cederquist, 1997) [half] [PS]
• Real numbers & analysis, Jan Cederquist,
• Semantics of first order languages based on formal topology (Henrik Persson) [ALF]

Other branches of mathematics

• The fundamental theorem of arithmetic. (Björn von Sydow, 1992) [ALF] [ALF, one file] [PS]
• Higman's lemma (Daniel Fridlender, 1997) [ALF] [PS]
• Intuitionistic version of Ramsey's theorem. (Daniel Fridlender, 1993) [ALF] [PS]

Misc

• Consistency in ALF (Thorsten Altenkirch, 1994) [PS]
• Computer based verification with ALF. (Thorsten Altenkirch,1996) A course in Munich University.
• a tactic for commutative monoid via 2-level approach. (Makoto Takeyama) [Agda]

Libraries

• ALF library (a summary of what had been done by 1994) [ALF] [PS] [DVI] [HTML]
• ALF Micro library (Thorsten Altenkirch,1995)
• HALF library (Thierry Coquand, Henrik Persson, Ilya Beylin,1996);
  adopted to agda
• Alfa examples (Thomas Hallgren,1998)
• Agda micro library (Catarina Coquand,1999) will become public soon

Related