2013•Unpublished venueRequires access
Type-theory in color
Jean-Philippe Bernardy, Guilhem Moulin
Open publisher page 28 citations
Abstract
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.