Canonical Structures of Coq
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
- About seminars
25 May 2020Retrofitting Parallelism onto OCaml
18 May 2020Heap Reference Compression in GraalVM Native Image
27 April 2020The expressive power of higher-order types and non-determinism
13 April 2020Model Checking under Weak Memory Models
16 March 2020Duplicate detection via semi-local lcs and sequence alignment