Proofs for free
Top Cited Papers
- 30 March 2012
- journal article
- research article
- Published by Cambridge University Press (CUP) in Journal of Functional Programming
- Vol. 22 (2), 107-152
- https://doi.org/10.1017/s0956796812000056
Abstract
Reynolds' 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.Keywords
This publication has 11 references indexed in Scilit:
- Parametricity, type equality, and higher-order polymorphismJournal of Functional Programming, 2010
- Free theorems involving type constructor classesPublished by Association for Computing Machinery (ACM) ,2009
- The Girard–Reynolds isomorphism (second edition)Theoretical Computer Science, 2007
- Inductive definitions in the system Coq rules and propertiesPublished by Springer Science and Business Media LLC ,2005
- The view from the leftJournal of Functional Programming, 2004
- Inductive familiesFormal Aspects of Computing, 1994
- Formal parametric polymorphismPublished by Association for Computing Machinery (ACM) ,1993
- Types, abstraction, and parametric polymorphism, part 2Lecture Notes in Computer Science, 1992
- Automatic synthesis of typed Λ-programs on term algebrasTheoretical Computer Science, 1985
- A formulation of the simple theory of typesThe Journal of Symbolic Logic, 1940