Proofs for Free -- Parametricity for Dependent Types

J-P Bernardy, P Jansson, R Paterson

Short summary for unicode lovers:

  ⟦_⟧ : PTS → PTS
  Γ ⊢ A : B   ⇒   ⟦Γ⟧ ⊢ ⟦A⟧ : ⟦B⟧ Ā

where

  ⟦A⟧    is the free proof and 
  ⟦B⟧ Ā  is the free theorem

2012-03-30: JFP FirstView online version available

Here is the bibtex entry:

  @Article{bernardy_proofs_2012,
	author = {Jean-Philippe Bernardy and Patrik Jansson and Ross Paterson},
	title = {Proofs for Free --- Parametricity for Dependent Types},
	journal = {Journal of Functional Programming},
	doi = {10.1017/S0956796812000056},
	year = {2012},
	volume = {22},
	number = {02},
	pages = {107--152},
	url     = {https://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=135303}
  },

2012-02-07: Extended journal version accepted for publication in JFP 2012.
2010-12-23: Extended journal version in submission.

Abstract

Reynolds’ abstraction theorem [1] 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.

[1] Reynolds, J. C. (1983) Types, abstraction and parametric polymorphism, Inf. Process. 83(1), 513–523

2010-06-09: ICFP 2010 paper: "Parametricity and Dependent Types" [ Bernardy, Jansson, Paterson ]
- ACM portal: http://portal.acm.org/citation.cfm?id=1863543.1863592
- BibTeX
@inproceedings{bernardy_parametricity_2010,

	author = {Jean-Philippe Bernardy and Patrik Jansson and Ross Paterson},
	address = {Baltimore, Maryland},
	title = {Parametricity and Dependent Types},
	booktitle = {Proceedings of {ICFP} 2010},
	publisher = {{ACM}},
	pages = {345--356},
	year = {2010}

Proofs for Free -- Parametricity for Dependent Types

Abstract

Links