Search: onr:"swepub:oai:research.chalmers.se:94d8d251-423c-485e-94c3-e217d5bf0015" >
Parametricity and D...
-
Bernardy, Jean-Philippe,1978Chalmers tekniska högskola,Chalmers University of Technology
(author)
Parametricity and Dependent Types
- Article/chapterEnglish2010
Publisher, publication year, extent ...
-
2010-09-27
-
Association for Computing Machinery (ACM),2010
Numbers
-
LIBRIS-ID:oai:research.chalmers.se:94d8d251-423c-485e-94c3-e217d5bf0015
-
https://doi.org/10.1145/1932681.1863592DOI
-
https://research.chalmers.se/publication/172124URI
Supplementary language notes
-
Language:English
-
Summary in:English
Part of subdatabase
Classification
-
Subject category:art swepub-publicationtype
-
Subject category:ref swepub-contenttype
Notes
-
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 (in second order predicate logic) about inhabitants of the type. We obtain a similar result for a single lambda calculus (a pure type system), in which terms, types and their relations are expressed. Working within a single system dispenses with the need for an interpretation layer, allowing for an unusually simple presentation. While the unification puts some constraints on the type system (which we spell out), the result applies to many interesting cases, including dependently-typed ones.
Subject headings and genre
Added entries (persons, corporate bodies, meetings, titles ...)
-
Jansson, Patrik,1972Chalmers tekniska högskola,Chalmers University of Technology(Swepub:cth)patrikj
(author)
-
Paterson, Ross
(author)
-
Chalmers tekniska högskola
(creator_code:org_t)
Related titles
-
In:SIGPLAN Notices (ACM Special Interest Group on Programming Languages): Association for Computing Machinery (ACM)45:9, s. 345-3560730-85660362-13401558-1160
Internet link
Find in a library
To the university's database