Canonical Structures of Coq

11 November 2019

The mechanism of Canonical Structures of Coq enables the formalizer to control type inference,
model typeclasses, synthesize proofs. Programmable type inference is one of the key ingredients
for the successful formalization of the Odd Order Theorem and is being widely used in the Mathcomp library.

On concrete examples we will show the inner workings of Coq's unification algorithm,
touch upon the questions of organizing algebraic hierarchies, and briefly compare
the language of Canonical Structures to the one of Type Classes and Unification Hints.

Presenter: Anton Trunov

Resources