scholarly journals Proofs for free

2012 ◽  
Vol 22 (2) ◽  
pp. 107-152 ◽  
Author(s):  
JEAN-PHILIPPE BERNARDY ◽  
PATRIK JANSSON ◽  
ROSS PATERSON
Keyword(s):  
Programming Language ◽  
Predicate Logic ◽  
Type Systems ◽  
Second Order ◽  
Pure Type ◽  
Parametric Polymorphism ◽  
Pure Type Systems ◽  
System F

AbstractReynolds' abstraction theorem (Reynolds, J. C. (1983) Types, abstraction and parametric polymorphism, Inf. Process.83(1), 513–523) shows how a typing judgement in System F can be translated into a relational statement (in second-order predicate logic) about inhabitants of the type. We obtain a similar result for pure type systems (PTSs): for any PTS used as a programming language, there is a PTS that can be used as a logic for parametricity. Types in the source PTS are translated to relations (expressed as types) in the target. Similarly, values of a given type are translated to proofs that the values satisfy the relational interpretation. We extend the result to inductive families. We also show that the assumption that every term satisfies the parametricity condition generated by its type is consistent with the generated logic.

ON THE CONSERVATIVITY OF LEIBNIZ EQUALITY

1998 ◽  
Vol 09 (04) ◽  
pp. 431-454
Author(s):  
M. P. A. SELLINK
Keyword(s):  
Type System ◽  
Type Systems ◽  
Order Theory ◽  
Second Order ◽  
First Order ◽  
Pure Type ◽  
First Order Theory ◽  
Pure Type Systems ◽  
Leibniz Equality

We embed a first order theory with equality in the Pure Type System λMON2 that is a subsystem of the well-known type system λPRED2. The embedding is based on the Curry-Howard isomorphism, i.e. → and ∀ coincide with → and Π. Formulas of the form [Formula: see text] are treated as Leibniz equalities. That is, [Formula: see text] is identified with the second order formula ∀ P. P(t1)→ P(t2), which contains only →'s and ∀'s and can hence be embedded straightforwardly. We give a syntactic proof — based on enriching typed λ-calculus with extra reduction steps — for the equivalence between derivability in the logic and inhabitance in λMNO2. Familiarity with Pure Type Systems is assumed.

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