{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T20:11:26Z","timestamp":1770322286633,"version":"3.49.0"},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2012,3,30]],"date-time":"2012-03-30T00:00:00Z","timestamp":1333065600000},"content-version":"unspecified","delay-in-days":29,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2012,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Reynolds' abstraction theorem (Reynolds, J. C. (1983) Types, abstraction and parametric polymorphism,<jats:italic>Inf. Process.<\/jats:italic><jats:bold>83<\/jats:bold>(1), 513\u2013523) 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.<\/jats:p>","DOI":"10.1017\/s0956796812000056","type":"journal-article","created":{"date-parts":[[2012,3,30]],"date-time":"2012-03-30T15:27:34Z","timestamp":1333121254000},"page":"107-152","source":"Crossref","is-referenced-by-count":66,"title":["Proofs for free"],"prefix":"10.1017","volume":"22","author":[{"given":"JEAN-PHILIPPE","family":"BERNARDY","sequence":"first","affiliation":[]},{"given":"PATRIK","family":"JANSSON","sequence":"additional","affiliation":[]},{"given":"ROSS","family":"PATERSON","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2012,3,30]]},"reference":[{"key":"S0956796812000056_ref25","first-page":"361","volume-title":"the Proceedings of TLCA '93, (Utrecht, The Netherlands, March 16\u201318)","author":"Plotkin","year":"1993"},{"key":"S0956796812000056_ref15","first-page":"63","article-title":"The impact of seq on free theorems-based program transformations","volume":"69","author":"Johann","year":"2006","journal-title":"Fundam. Inf."},{"key":"S0956796812000056_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"S0956796812000056_ref20","first-page":"277","volume-title":"the Proceedings of the Twenty-Fourth IEEE Symposium on Logic in Computer Science","author":"Morris","year":"2009"},{"key":"S0956796812000056_ref16","first-page":"313","volume-title":"the Proceedings of FPCA 1991 (Cambridge, MA, August 26\u201330)","author":"Mairson","year":"1991"},{"key":"S0956796812000056_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158622"},{"key":"S0956796812000056_ref22","unstructured":"Norell U. (2007) Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Chalmers Tekniska H\u00f6gskola, Gothenburg, Sweden."},{"key":"S0956796812000056_ref3","unstructured":"Bernardy J.-P. (2010) Lightweight free theorems: Agda library. Accessed March 13, 2012. Available at: http:\/\/wiki.portal.chalmers.se\/agda\/agda.php?n=Libraries.LightweightFreeTheorems"},{"key":"S0956796812000056_ref8","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S0956796812000056_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90135-5"},{"key":"S0956796812000056_ref23","first-page":"39","volume-title":"the Proceedings of ICFP 2008 (Victoria, BC, Canada, September 20\u201328)","author":"Oury","year":"2008"},{"key":"S0956796812000056_ref33","first-page":"60","volume-title":"the Proceedings of POPL'89 (Austin, TX, January 11\u201313)","author":"Wadler","year":"1989"},{"key":"S0956796812000056_ref12","first-page":"85","volume-title":"the Proceedings of WGP 2009 (Edinburgh, UK, August 30)","author":"Gibbons","year":"2009"},{"key":"S0956796812000056_ref30","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796810000079"},{"key":"S0956796812000056_ref31","first-page":"347","volume-title":"the Proceedings of FPCA 1989 (London, UK, September 11\u201313)","author":"Wadler","year":"1989"},{"key":"S0956796812000056_ref27","first-page":"513","article-title":"Types, abstraction and parametric polymorphism","volume":"83","author":"Reynolds","year":"1983","journal-title":"Inf. Process."},{"key":"S0956796812000056_ref29","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1145\/1596550.1596577","volume-title":"the Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (Edinburgh, UK, August 31\u2013September 2)","author":"Voigtl\u00e4nder","year":"2009"},{"key":"S0956796812000056_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.042"},{"key":"S0956796812000056_ref5","first-page":"108","volume-title":"the Proceedings of FoSSaCS 2011","author":"Bernardy","year":"2011"},{"key":"S0956796812000056_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037116"},{"key":"S0956796812000056_ref21","first-page":"135","volume-title":"Proceedings of ICFP 2009 (Los Angeles, August)","author":"Neis","year":"2009"},{"key":"S0956796812000056_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"S0956796812000056_ref4","first-page":"345","volume-title":"Proceedings of ICFP 2010 (Baltimore, MD, September 27\u201329)","author":"Bernardy","year":"2010"},{"key":"S0956796812000056_ref7","unstructured":"B\u00f6hme S. (2007) Free Theorems for Sublanguages of Haskell. Master's thesis, Technische Universit\u00e4t Dresden, Netherlands."},{"key":"S0956796812000056_ref19","first-page":"1","volume-title":"the Proceedings of PLPV 2010 (Madrid, Spain, January 19)","author":"Monnier","year":"2010"},{"key":"S0956796812000056_ref10","unstructured":"Coquand T. (1992) Pattern matching with dependent types. In the Proceedings of the Workshop on Types for Proofs and Programs (Torino, Italy), pp. 66\u201379."},{"key":"S0956796812000056_ref28","unstructured":"The Coq Development Team. (2010) The Coq Proof Assistant. Reference manual. Available at: http:\/\/www.coq.inria.fr\/doc"},{"key":"S0956796812000056_ref18","volume-title":"Le Calcul des Constructions Implicite: Syntaxe et S\u00e9mantique","author":"Miquel","year":"2001"},{"key":"S0956796812000056_ref26","doi-asserted-by":"crossref","first-page":"320","DOI":"10.1145\/2034773.2034817","volume-title":"the Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP '11 (Tokyo, Japan, September 19\u201321)","author":"Pouillard","year":"2011"},{"key":"S0956796812000056_ref9","first-page":"227","volume-title":"Logic in Computer Science","author":"Coquand","year":"1986"},{"key":"S0956796812000056_ref13","unstructured":"Girard J.-Y. (1972) Interpr\u00e9tation Fonctionnelle et Elimination Des Coupures de L'arithm\u00e9tique D'ordre Sup\u00e9rieur, Th\u00e8eses d'\u00e9tat, Universit\u00e9 de Paris, Paris, France."},{"key":"S0956796812000056_ref14","first-page":"83","volume-title":"Venice Festschrift","author":"Hofmann","year":"1996"},{"key":"S0956796812000056_ref2","first-page":"117","article-title":"Lambda calculi with types","volume":"2","author":"Barendregt.","year":"1992","journal-title":"Handbook Log. Comput. Sci."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796812000056","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,9]],"date-time":"2022-01-09T10:53:19Z","timestamp":1641725599000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796812000056\/type\/journal_article"}},"subtitle":["Parametricity for dependent types"],"short-title":[],"issued":{"date-parts":[[2012,3]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,3]]}},"alternative-id":["S0956796812000056"],"URL":"https:\/\/doi.org\/10.1017\/s0956796812000056","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,3]]}}}