Hostname: page-component-8448b6f56d-tj2md Total loading time: 0 Render date: 2024-04-23T13:58:20.243Z Has data issue: false hasContentIssue false
  • English
  • Français

Domain-free pure type systems

Published online by Cambridge University Press:  03 November 2000

GILLES BARTHE  and
MORTEN HEINE SØRENSEN
GILLES BARTHE
Affiliation:
INRIA Sophia-Antipolis, 2004 Route des Lucioles, BP 93, 06902 Sophia-Antipolis Cedex, France (e-mail: Gilles.Barthe@sophia.inria.fr)
MORTEN HEINE SØRENSEN
Affiliation:
Department of Computer Science, University of Copenhagen (DIKU), Universitetsparken 1, DK-2100 Copenhagen Ø, Denmark (e-mail: rambo@diku.dk)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Pure type systems make use of domain-full λ-abstractions λx:D.M. We present a variant of pure type systems, which we call domain-free pure type systems, with domain-free λ-abstractions λx.M. Domain-free pure type systems have a number of advantages over both pure type systems and so-called type assignment systems (they also have some disadvantages), and have been used in theoretical developments as well as in implementations of proof-assistants. We study the basic properties of domain-free pure type systems, establish their formal relationship with pure type systems and type assignment systems, and give a number of applications of these correspondences.

Type
Research Article
Information
Journal of Functional Programming , Volume 10 , Issue 5 , September 2000 , pp. 417 - 452
Copyright
© 2000 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.