Pure type systems with explicit substitution

2001 ◽  
Vol 11 (1) ◽  
pp. 3-19 ◽  
Author(s):  
ROEL BLOO
Keyword(s):  
Type Systems ◽  
Pure Type ◽  
Reduction Property ◽  
Explicit Substitution ◽  
Pure Type Systems

We define an extension of pure type systems with explicit substitution. We show that the type systems with explicit substitution are strongly normalizing iff their ordinary counterparts are. Subject reduction is shown to fail in general but a weaker, though still useful, subject reduction property is established. A more complicated extension is proposed for which subject reduction does hold in general.

Pure type systems with explicit substitutions

2015 ◽  
Vol 25 ◽  
Author(s):  
DANIEL FRIDLENDER ◽  
MIGUEL PAGANO
Keyword(s):  
Type Systems ◽  
Pure Type ◽  
Explicit Substitution ◽  
Explicit Substitutions ◽  
Pure Type Systems ◽  
De Bruijn ◽  
New Formulation ◽  
De Bruijn Indices ◽  
Meta Theory

AbstractWe 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 η.

scholarly journals Automath and Pure Type Systems

2003 ◽  
Vol 85 (7) ◽  
pp. 30-49
Author(s):  
Fairouz Kamareddine ◽  
Twan Laan ◽  
Rob Nederpelt
Keyword(s):  
Type Systems ◽  
Pure Type ◽  
Pure Type Systems

scholarly journals Weak normalization implies strong normalization in a class of non-dependent pure type systems

2001 ◽  
Vol 269 (1-2) ◽  
pp. 317-361 ◽  
Author(s):  
Gilles Barthe ◽  
John Hatcliff ◽  
Morten Heine Sørensen
Keyword(s):  
Type Systems ◽  
Strong Normalization ◽  
Pure Type ◽  
Pure Type Systems

scholarly journals Pure Type Systems without Explicit Contexts

2010 ◽  
Vol 34 ◽  
pp. 53-67 ◽  
Author(s):  
Herman Geuvers ◽  
Robbert Krebbers ◽  
James McKinna ◽  
Freek Wiedijk
Keyword(s):  
Type Systems ◽  
Pure Type ◽  
Pure Type Systems

Pure Type Systems with de Bruijn Indices

2002 ◽  
Vol 45 (2) ◽  
pp. 187-201 ◽  
Author(s):  
F. Kamareddine
Keyword(s):  
Type Systems ◽  
Pure Type ◽  
Pure Type Systems ◽  
De Bruijn ◽  
De Bruijn Indices

scholarly journals Pure Type System conversion is always typable

2012 ◽  
Vol 22 (2) ◽  
pp. 153-180 ◽  
Author(s):  
VINCENT SILES ◽  
HUGO HERBELIN
Keyword(s):  
Type System ◽  
Type Systems ◽  
Positive Answer ◽  
General Question ◽  
Pure Type ◽  
Typing System ◽  
Long Time ◽  
Pure Type Systems

AbstractPure Type Systems are usually described in two different ways, one that uses an external notion of computation like beta-reduction, and one that relies on a typed judgment of equality, directly in the typing system. For a long time, the question was open to know whether both presentations described the same theory. A first step towards this equivalence has been made by Adams for a particular class ofPure Type Systems(PTS) called functional. Then, his result has been relaxed to all semi-full PTSs in previous work. In this paper, we finally give a positive answer to the general question, and prove that equivalence holds for any Pure Type System.

Sign in / Sign up

Export Citation Format

Share Document