transparent gif

 

Ej inloggad.

Göteborgs universitets publikationer

Proofs for Free -- Parametricity for dependent types

Författare och institution:
Jean-Philippe Bernardy (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers), Chalmers & Institutionen för data- och informationsteknik (GU)); Patrik Jansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers), Chalmers & Institutionen för data- och informationsteknik (Chalmers), Chalmers); Ross Paterson (-)
Publicerad i:
Journal of Functional Programming, 22 ( 2 ) s. 107-152
ISSN:
0956-7968
Antal sidor:
37
Publikationstyp:
Artikel, refereegranskad vetenskaplig
Publiceringsår:
2012
Språk:
engelska
Fulltextlänk:
Fulltextlänk (lokalt arkiv):
Sammanfattning (abstract):
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.
Ämne (baseras på Högskoleverkets indelning av forskningsämnen):
NATURVETENSKAP ->
Data- och informationsvetenskap ->
Datavetenskap (datalogi) ->
Teoretisk datalogi
NATURVETENSKAP ->
Data- och informationsvetenskap ->
Datavetenskap (datalogi) ->
Datalogi
Chalmers styrkeområden:
Informations- och kommunikationsteknik
Chalmers fundament:
Grundläggande vetenskaper
Postens nummer:
135303
Posten skapad:
2011-01-20 09:27
Posten ändrad:
2016-08-18 14:08

Visa i Endnote-format

Göteborgs universitet • Tel. 031-786 0000
© Göteborgs universitet 2007