A Cut-Free Sequent Calculus for Pure Type Systems Verifying the Structural Rules of Gentzen/Kleene

2003 ◽  
pp. 17-31 ◽  
Author(s):  
Francisco Gutiérrez ◽  
Blas Ruiz
Keyword(s):  
Sequent Calculus ◽  
Type Systems ◽  
Structural Rules ◽  
Pure Type ◽  
Pure Type Systems

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