CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Type-Theory In Color

Jean-Philippe Bernardy (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Guilhem Moulin (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
ACM SIGPLAN Notices (0362-1340). Vol. 48 (2013), 9, p. 61-71.
[Artikel, refereegranskad vetenskaplig]

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.

Nyckelord: type-theory, parametricity, erasure

Denna post skapades 2014-01-08. Senast ändrad 2014-01-20.
CPL Pubid: 191836


Läs direkt!

Länk till annan sajt (kan kräva inloggning)