Names For Free — Polymorphic Views of Names and Binders Jean-Philippe Bernardy Chalmers University of Technology and University of Gothenburg bernardy@chalmers.se Nicolas Pouillard IT University Copenhagen npou@itu.dk Abstract We propose a novel technique to represent names and binders in Haskell. The dynamic (run-time) representation is based on de Bruijn indices, but it features an interface to

Type-Theory In Color Jean-Philippe Bernardy Guilhem Moulin Chalmers University of Technology and University of Gothenburg {bernardy,mouling}@chalmers.se Abstract Dependent type-theory aims to become the standard way to formal- ize mathematics at the same time as displacing traditional platforms for high-assurance programming. However, current implementa- tions of type theory are still lacking, in