TYPE INFERENCE FOR PURE TYPE SYSTEMS

Authors
SEVERI P
Citation
P. Severi, TYPE INFERENCE FOR PURE TYPE SYSTEMS, Information and computation, 143(1), 1998, pp. 1-23
Citations number
10
Categorie Soggetti
Mathematics,"Computer Science Information Systems",Mathematics,"Computer Science Information Systems
Journal title
Information and computation → ACNP
ISSN journal
08905401
Volume
143
Issue
1
Year of publication
1998
Pages
1 - 23
Database
ISI
SICI code
0890-5401(1998)143:1<1:TIFPTS>2.0.ZU;2-V
Abstract
In this paper we define a type inference semi-algorithm for singly sor ted pure type systems. For that, we define the notion of pure type sys tems without the Pi-condition and a mapping from pure type systems wit hout the Pi-condition to pure type systems. This allows us to prove th e two main results: first that weak normalisation is preserved by the extension and second the correctness of the type inference semi-algori thm. (C) 1998 Academic Press.