Abstract
The first seminar was a defense and illustration of programming with dependent types in the Agda language. The speaker started from a classical problem : the semantics of an arithmetic expression language and its compilation into the code of a stack machine. He showed that many error cases have to be dealt with if only simple types are used, but disappear if expressions and machine instructions are indexed by the types of the values produced. By construction, this ensures that the compiler preserves types. Instructions can also be indexed by their operational semantics, which by construction guarantees that the compiler is correct (preserves semantics), thus reaching an extreme point of type-dependent programming.
