[Prev][Next][Index][Thread]
Paper on Using Types for Termination Checking
-
To: types@cis.upenn.edu
-
Subject: Paper on Using Types for Termination Checking
-
From: Andreas Abel <abel@informatik.uni-muenchen.de>
-
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
Hi,
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
ABSTRACT:
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
http://www.tcs.informatik.uni-muenchen.de/~abel/
--Andreas Abel
--
Andreas Abel --<>-- What if Jesus is right?
Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/