Below you find some implementations of lambda calculi and logics that
are no longer actively developed.
Tutch is apparently used for teaching logics
at some universities; email me if you find bugs.
- Type Checker for Curry-style System Fω
Type-checking is easy for fully type-annotated (Church-style) terms of
Girard's System Fω but undecidable for non-annotated
(Curry-style) terms. Hence, the type checker we implemented is
necessary incomplete. Nevertheless, it succeeds on most typical terms
occurring in Fω programs and has proven to be a practical
tool for my own purposes.
- B. Pierce's fomega: Church-style type checker (no longer supported)
- C. Raffalli's type checkers for System Fη
- Type Checker for Church-style System Fω
This type checker does the (rather) simple job of checking fully annotated
lambda-terms of System Fω. It is envisioned as a
double-checking backend to the Fomega checker (see above).
- Tutorial Proof Checker
tutch is a proof CHecker for TUTorial purposes. It is based on
intutionistic logic and supports the following proof forms:
...and the following theories:
- natural deduction (ND) proofs
- ND proofs annotated with proof terms
- proof terms
- intuitionistic and classical propositional logic
- intuitionistic pure first-order logic
- Heyting Arithmetic (booleans, natural numbers, lists)
Publication on tutch
Human-Readable Machine-Verifiable Proofs for
Teaching Constructive Logic
Andreas Abel, Bor-Yuh Evan Chang and Frank Pfenning
Proof Transformations, Proof Presentations and Complexity of Proofs
- Termination Checker for Functional Programs
foetus is a type-theoretic functional programming language, a
simplification of MuTTI (Munich Type Theory Implementation), designed
to investigate termination checking of recursive functions. An
implementation of the termination checker has been carried out in
1997/1998 and is accessible via the WWW. In
my diploma thesis (1999), I proved wellfoundedness of the structural
term ordering used in foetus. A predicative version (in
the sense of Martin-Löf's type theory) of the proof appeared in
the Journal of Functional Programming (2002) and a soundness
proof of the static analysis algorithm of foetus has been
published in the proceedings of TYPES'99.
Drafts and Publications on foetus
- A Predicative Analysis of Structural Recursion
Andreas Abel and Thorsten Altenkirch (2002)
Journal of Functional Programming 12(1):1-41.
Specification and Verification of a
Formal System for Structurally Recursive Functions
Andreas Abel (2000)
Types for Proofs and Programs, International Workshop, TYPES '99
Lökeberg, Sweden, June 1999.
- A Semantic Analysis of Structural Recursion
Andreas Abel (1999)
Diploma Thesis, Ludwig-Maximilians-University, Munich.
- foetus - Termination Checker for Simple
Andreas Abel (1998)
Implementation and Documentation.
Executable web version