Mechanise your proofs in Coq: From zero to cut-admissibility in less than three months.
In this talk, I will tell about my short experience on learning the basics of proof-mechanisation in the Coq poof assistant. As an example, I will show how I mechanised cut admissibility for the multiplicative fragment of intuitionistic linear logic.
Sat 6 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:00
|Proving properties about Linear Pi in Coq
|Binary Session Types in Coq
Ornela Dardha University of Glasgow
|Mechanise your proofs in Coq: From zero to cut-admissibility in less than three months.
Marco Carbone IT University of Copenhagen