Type-Theory in Color
Författare och institution:
Jean-Philippe Bernardy (Institutionen för data- och informationsteknik, Programvaruteknik); Guilhem Moulin (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik)
Antal sidor:
10
Publikationstyp:
Preprint
Publiceringsår:
2012
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
Matematik ->
Algebra och logik ->
Matematisk logik
NATURVETENSKAP ->
Data- och informationsvetenskap ->
Datavetenskap (datalogi) ->
Teoretisk datalogi
Chalmers styrkeområden:
Informations- och kommunikationsteknik
Chalmers fundament:
Grundläggande vetenskaper
Postens nummer:
164608
Posten skapad:
2012-10-11 14:12
Posten ändrad:
2013-02-15 08:40