To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

A Presheaf Model of Param… - University of Gothenburg, Sweden Till startsida
Sitemap
To content Read more about how we use cookies on gu.se

A Presheaf Model of Parametric Type Theory

Journal article
Authors Jean-Philippe Bernardy
Thierry Coquand
Guilhem Moulin
Published in Electronical Notes in Theoretical Computer Science
Volume 319
Pages 67-82
ISSN 1571-0661
Publication year 2015
Published at Department of Computer Science and Engineering, Computing Science, Programming Logic
Pages 67-82
Language en
Links dx.doi.org/10.1016/j.entcs.2015.12....
https://gup.ub.gu.se/file/178162
Keywords Parametricity, Presheaf semantics, Type theory
Subject categories Theoretical computer science

Abstract

We extend Martin-Löf's Logical Framework with special constructions and typing rules providing internalized parametricity. Compared to previous similar proposals, this version comes with a denotational semantics which is a refinement of the standard presheaf semantics of dependent type theory. Further, this presheaf semantics is a refinement of the one used to interpret nominal sets with restrictions. The present calculus is a candidate for the core of a proof assistant with internalized parametricity.

Page Manager: Webmaster|Last update: 9/11/2012
Share:

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?