Paper on Using Types for Termination Checking

I'd like to announce the availability of a new technical report.  All
kinds of comments are very welcome.

TITLE:  Termination Checking with Types
AUTHOR: Andreas Abel

Recently, types have been discovered for termination checking.  Xi
[LICS 2001] uses dependent types, whereas Gim'enez [ICALP 1998]
presented an extension of the Calculus of Constructions with guarded
types, subtyping and bounded quantification.  However, no proofs of
subject reduction and normalization were supplied.  We adapted his
system to simply-typed functional programming (omitting corecursion).
In the technical report, we give proofs of type preservation and
strong normalization.  Furthermore, we present a surprisingly simple
bidirectional type-checking algorithm which encompasses termination
checking and some size analysis.

The technical report is available under


--Andreas Abel

Andreas Abel     --<>--    What if Jesus is right? 

Theoretical Computer Science, University of Munich