Pure type systems with explicit substitutions. (9th November 2015)

• Record Type: Journal Article
• Authors: FRIDLENDER, DANIEL; PAGANO, MIGUEL
• Is Part Of: Journal of functional programming. Volume 25(2015)
• Publication Date: 2015-11-09
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796815000210
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: We introduce a new formulation of pure type systems (PTSs) with explicit substitution and de Bruijn indices and formally prove some of its meta-theory. Using techniques based on Normalisation by Evaluation, we prove that untyped conversion can be typed for predicative PTSs. Although this equivalence was settled by Siles and Herbelin for the conventional presentation of PTSs, we strongly conjecture that our proof method can also be applied to PTSs with η.