Sökning: 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
(författare)
Parametricity and Dependent Types
- Artikel/kapitelEngelska2010
Förlag, utgivningsår, omfång ...
-
2010-09-27
-
Association for Computing Machinery (ACM),2010
Nummerbeteckningar
-
LIBRIS-ID:oai:research.chalmers.se:94d8d251-423c-485e-94c3-e217d5bf0015
-
https://doi.org/10.1145/1932681.1863592DOI
-
https://research.chalmers.se/publication/172124URI
Kompletterande språkuppgifter
-
Språk:engelska
-
Sammanfattning på:engelska
Ingår i deldatabas
Klassifikation
-
Ämneskategori:art swepub-publicationtype
-
Ämneskategori:ref swepub-contenttype
Anmärkningar
-
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.
Ämnesord och genrebeteckningar
Biuppslag (personer, institutioner, konferenser, titlar ...)
-
Jansson, Patrik,1972Chalmers tekniska högskola,Chalmers University of Technology(Swepub:cth)patrikj
(författare)
-
Paterson, Ross
(författare)
-
Chalmers tekniska högskola
(creator_code:org_t)
Sammanhörande titlar
-
Ingår i:SIGPLAN Notices (ACM Special Interest Group on Programming Languages): Association for Computing Machinery (ACM)45:9, s. 345-3560730-85660362-13401558-1160
Internetlänk
Hitta via bibliotek
Till lärosätets databas