Paper on Using Types for Termination Checking
Subject: Paper on Using Types for Termination Checking
From: Andreas Abel <firstname.lastname@example.org>
Date: Fri, 11 Jan 2002 18:21:05 +0100
Organization: LMU Muenchen
User-Agent: Mozilla/5.0 (X11; U; Linux 2.4.4-4GB i686; en-US; 0.8.1) Gecko/20010515
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 --<>-- What if Jesus is right?
Theoretical Computer Science, University of Munich