CPL - Chalmers Publication Library

Type-Theory in Color

Författare och institution:
Jean-Philippe Bernardy (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)); Guilhem Moulin (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers))
Publicerad i:
18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013; Boston, MA; United States; 25 September 2013 through 27 September 2013, s. 61-71
ISBN:
978-145032326-0
Antal sidor:
10
Publikationstyp:
Konferensbidrag, refereegranskat
Publiceringsår:
2013
Språk:
engelska
Fulltextlänk:
Sammanfattning (abstract):
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.
Ämne (baseras på Högskoleverkets indelning av forskningsämnen):
NATURVETENSKAP ->
Matematik ->
Algebra och logik ->
Matematisk logik
NATURVETENSKAP ->
Data- och informationsvetenskap ->
Datavetenskap (datalogi) ->
Teoretisk datalogi
Nyckelord:
type-theory, parametricity, erasure
Chalmers styrkeområden:
Informations- och kommunikationsteknik
Chalmers fundament:
Grundläggande vetenskaper
Postens nummer:
164608
Posten skapad:
2012-10-11 14:12
Posten ändrad:
2014-01-20 14:41

Visa i Endnote-format