University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Teaching Mechanized Semantics

Teaching Mechanized Semantics

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact nobody.

VSO2 - Verified software

“Mechanized Semantics” is a course I taught at Collège de France in 2019-2020 (https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fxavierleroy.org%2FCdF%2F2019-2020%2F&data=05%7C01%7CAnnie.Bacon%40newton.ac.uk%7C3a72cc5ee0a84105a47608da6982ad51%7C49a50445bdfa4b79ade3547b4f3986e9%7C0%7C0%7C637938307206974330%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=pcb4vRIMmGJFqzN5eD0e0cvJj2vidqyxMY54FP%2FFIGU%3D&reserved=0) that tries to show why and how interactive theorem proving is increasingly used for P.L. research, and to illustrate the approaches by mechanizing in Coq most of Nielson and Nielson’s textbook “Semantics with applications: an appetizer”.  The course focuses on how to go from high-level intuitions and historical perspectives to the formal definitions and theorem statements; how to conduct the proofs was barely mentioned.  I’ll discuss what worked well and what worked not so well with this approach.

This talk is part of the Isaac Newton Institute Seminar Series series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2022 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity