Teaching Mechanized Semantics

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

• Xavier Leroy (Collège de France)
• Wednesday 20 July 2022, 14:30-15:00
• Seminar Room 2, Newton Institute.

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.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 2, Newton Institute
• bld31

Note that ex-directory lists are not shown.