Ambrus Kaposi
April 26–27, 2017, Nantes, France
Meeting in the framework of the COST Action EUTypes .
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 (du
Ambrus Kaposi