EUTypes WG1 meeting, Nantes, France, 26-27 April 2017
Proof assistants are now state of the art tools for formalizing mathematical reasoning, both for the verification of proofs in mathematics itself and for the verification of software and hardware in computer science. Various proof assistants are based on type theory and it turns out that powerful type theory provide a rich language for capturing notions from computer science and mathematics, ranging from very algorithmic notions (correctness of programs) to very abstract mathematics like homotopy theory (due to the recent advances in Homotopy Type Theory).
For this workshop we have invited researchers in formalizing mathematics and proof assistants based on dependent type theory, homotopy type theory, higher inductive types and cubical type theory, to discuss how type-based proof assistant can be used for the practical formalization and verification of mathematical proofs.
This workshop is organised and funded by the COST EUTypes project (https://eutypes.cs.ru.nl/).
