## Guilhem Moulin (Chalmers, Sweden), Type Theory in Colors

### Programme

- 14 février 2013, 14:00 - 15:00

### Résumé

Dependent type-theory is becoming the standard way to formalize mathematics, at the same time as displacing traditional platforms for high-insurance programming.

However, current implementations of type-theory are not always satisfactory in the sense that some "obvious truth" are impossible to prove, making type-theory awkward to use for many applications, both in formalization and programming.

We propose an extension of type-theory with colored terms, a notion of color erasure, and an interpretation of colored types as predicates. That leads to a more powerful type-theory: Some proofs and definitions can now be trivially derived hence can be omitted; Beside, some parametricity results can be internalized. (Joint work with Jean-Philippe Bernardy.)