CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Proofs for Free -- Parametricity for dependent types

Jean-Philippe Bernardy (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers) ; Institutionen för data- och informationsteknik (GU)) ; Patrik Jansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers) ; Institutionen för data- och informationsteknik (Chalmers)) ; Ross Paterson
Journal of Functional Programming (0956-7968). Vol. 22 (2012), 2, p. 107-152 .
[Artikel, refereegranskad vetenskaplig]

Reynolds' abstraction theorem 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: 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. Our proof gives a computationally meaningful way to interpret that assumption.



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2011-01-20. Senast ändrad 2016-08-18.
CPL Pubid: 135303

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)

Länk till annan sajt (kan kräva inloggning)