Completed Projects
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.
Fomega
 Type Checker for Currystyle System F_{ω}

Typechecking is easy for fully typeannotated (Churchstyle) terms of
Girard's System F^{ω} but undecidable for nonannotated
(Currystyle) 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.
Related Projects
 B. Pierce's fomega: Churchstyle type checker (no longer supported)
 C. Raffalli's type checkers for System F^{η}
church
 Type Checker for Churchstyle System F_{ω}

This type checker does the (rather) simple job of checking fully annotated
lambdaterms of System F_{ω}. It is envisioned as a
doublechecking backend to the Fomega checker (see above).
tutch
 Tutorial Proof Checker

tutch is a proof CHecker for TUTorial purposes. It is based on
intutionistic logic and supports the following proof forms:
 natural deduction (ND) proofs
 ND proofs annotated with proof terms
 proof terms
...and the following theories:
 intuitionistic and classical propositional logic
 intuitionistic pure firstorder logic
 Heyting Arithmetic (booleans, natural numbers, lists)
Publication on tutch

HumanReadable MachineVerifiable Proofs for
Teaching Constructive Logic

Andreas Abel, BorYuh Evan Chang and Frank Pfenning
Proof Transformations, Proof Presentations and Complexity of Proofs
(PTP01). Workshop
Proceedings.
foetus
 Termination Checker for Functional Programs

foetus is a typetheoretic 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 MartinLö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):141.
©Cambridge University
Press
.pdf
.ps.gz
.dvi
.bib

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.
LNCS 1956.
©SpringerVerlag
.pdf
.ps.gz
.dvi
.bib
 A Semantic Analysis of Structural Recursion

Andreas Abel (1999)
Diploma Thesis, LudwigMaximiliansUniversity, Munich.
.pdf
.ps.gz
.dvi
.bib
 foetus  Termination Checker for Simple
Functional Programs

Andreas Abel (1998)
Implementation and Documentation.
.pdf
.ps.gz
.dvi
.bib
Executable web version
[ Home
 CV
 Projects
 Publications
 Talks
 Teaching
 Sharing
]
