Journal of Functional Programming



THEORETICAL PEARLS

Type-checking injective pure type systems


GILLES BARTHE a1
a1 INRIA Sophia Antipolis, 2004 Route des Lucioles, BP 93, 06902 Sophia Antipolis Cedex, France (e-mail: Gilles.Barthe@sophia.inria.fr)

Abstract

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 R:]M) and sort(Γ[mid R:]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 R:].) and sort(.[mid R:].), 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 R:].) and sort(.[mid R:].).


Dedication:
In memory of Yossi Shamir