Sökning: onr:"swepub:oai:research.chalmers.se:cb6fc5fd-3197-43b1-bfe0-6273bbc1e8e9" >
Type-Theory In Color
Type-Theory In Color
-
- Bernardy, Jean-Philippe, 1978 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Moulin, Guilhem, 1988 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
(creator_code:org_t)
- 2013-09-25
- 2013
- Engelska.
-
Ingår i: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - : Association for Computing Machinery (ACM). - 0730-8566 .- 0362-1340 .- 1558-1160. ; 48:9, s. 61-71
- Relaterad länk:
-
http://dx.doi.org/10...
-
visa fler...
-
https://research.cha...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- Dependent type-theory aims to become the standard way to formalize mathematics at the same time as displacing traditional platforms for high-assurance programming. However, current implementations of type theory are still lacking, in the sense that some obvious truths require explicit proofs, making type-theory awkward to use for many applications, both in formalization and programming. In particular, notions of erasure are poorly supported.In this paper we propose an extension of type-theory with colored terms, color erasure and interpretation of colored types as predicates. The result is a more powerful type-theory: some definitions and proofs may be omitted as they become trivial, it becomes easier to program with precise types, and some parametricity results can be internalized.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Nyckelord
- erasure
- type-theory
- parametricity
Publikations- och innehållstyp
- art (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas