Hostname: page-component-7c8c6479df-p566r Total loading time: 0 Render date: 2024-03-26T22:30:26.871Z Has data issue: false hasContentIssue false

Type-checking injective pure type systems

Published online by Cambridge University Press:  01 November 1999

GILLES BARTHE
Affiliation:
INRIA Sophia Antipolis, 2004 Route des Lucioles, BP 93, 06902 Sophia Antipolis Cedex, France (e-mail: Gilles.Barthe@sophia.inria.fr)
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.

Injective pure type systems form a large class of pure type systems for which one can compute by purely syntactic means two sorts elmt(Γ[mid ]M) and sort(Γ[mid ]M), where Γ is a pseudo-context and M is a pseudo-term, and such that for every sort s,

formula here

By eliminating the problematic clause in the (abstraction) rule in favor of constraints over elmt(.[mid ].) and sort(.[mid ].), we provide a sound and complete type-checking algorithm for injective pure type systems. In addition, we prove expansion postponement for a variant of injective pure type systems where the problematic clause in the (abstraction) rule is replaced in favor of constraints over elmt(.[mid ].) and sort(.[mid ].).

Type
THEORETICAL PEARLS
Copyright
© 1999 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.