A deep embedding of parametric polymorphism in Coq

Research output: Contribution to conferencePaper

Abstract

We describe a deep embedding of System F inside Coq, along with a denotational semantics that supports reasoning using Reynolds parametricity. The denotations of System F types are given exactly by objects of sort Set in Coq, and the relations used to formalise Reynolds parametricity are Coq predicates with values in Prop. A key feature of the model is the extensive use of dependent types to maintain agreement between the parts of the model. We use type dependency to represent well-formedness of types and terms, and to keep track of the relation between the denotations of types and the parametricity relations between them. We have used an extension of this formalisation in other research, where we proved that the parametric polymorphic representation of Higher-Order Abstract Syntax is adequate.
Original languageEnglish
Pages2
Publication statusPublished - 4 Sep 2009
Event4rd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory - Edinburgh, United Kingdom
Duration: 4 Sep 2009 → …
https://www.cis.upenn.edu/~bcpierce/wmm/wmm09.html

Workshop

Workshop4rd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory
Abbreviated titleWMM
CountryUnited Kingdom
CityEdinburgh
Period4/09/09 → …
Internet address

Keywords

  • parametric polymorphism
  • Reynolds parametricity

Fingerprint Dive into the research topics of 'A deep embedding of parametric polymorphism in Coq'. Together they form a unique fingerprint.

Cite this