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, Programmeringslogik (Chalmers))
18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013; Boston, MA; United States; 25 September 2013 through 27 September 2013 p. 61-71.
[Konferensbidrag, refereegranskat]

Dependent-type theory is on the verge of becoming the standard way to formalise mathematics at the same time as displace traditional platforms for high-insurance programming. However, current implementations of type theory are still lacking, in the sense that obvious truths are simply impossible to prove, making type-theory awkward to use for many applications, both in formalisation or programming. In particular, notions of erasure are poorly supported. In this paper we propose to conservatively extend type-theory with colored terms, color erasure and color selection. 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



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2012-10-11. Senast ändrad 2014-01-20.
CPL Pubid: 164608

 

Läs direkt!


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