Conversion and reduction in dependently-typed calculi

Time: Wed 2016-03-09 13:15
Room: Johanneberg, Gothenburg

Type-checking a dependently-typed language involves solving equality constraints between λ-terms. Reduction to a normal form is the first step before applying a unification procedure.

The goal of the talk to spur some discussion on which techniques show more promise to speed up the Agda implementation. Anyone with experience or an interest in the implementation of dependent type-checking is welcome.

Material

Future work