The foetus Project

foetus is type-theoretic functional programming language, a simplification of MuTTI (Munich Type Theory Implementation), designed to investigate how to check termination of recursive functions. A first implementation of the termination checker has been carried out in 1997/1998 and is accessible via the WWW. Then followed some theoretical studies to prove the soundness of foetus, including my diploma thesis in 1999. At the moment I am working on a complete formalization.

Drafts and Publications on foetus

Specification and Verification of a Formal System for Structurally Recursive Functions: Andreas Abel
January 2000, Submitted to TYPES`99.
A Predicative Analysis on Structural Recursion: Andreas Abel and Thorsten Altenkirch
December 1999, Submitted to JFP.
A Semantic Analysis of Structural Recursion: Andreas Abel's Master's Thesis
February 1999.
foetus - Termination Checker for Simple Functional Programs: Andreas Abel
July 1998, Web Resource.

[ Home | CV | Publications | Projects ]
[ Personal page | Home@LMU,Munich ]

abel@cs.cmu.edu
http://www.cs.cmu.edu/~abel