Abstract

“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.