BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Teaching Mechanized Semantics - Xavier Leroy (Collège de France)
DTSTART:20220720T133000Z
DTEND:20220720T140000Z
UID:TALK176822@talks.cam.ac.uk
DESCRIPTION:"Mechanized Semantics" is a course I taught at Coll&egrave\;ge
  de France in 2019-2020 (https://eur03.safelinks.protection.outlook.com/?u
 rl=https%3A%2F%2Fxavierleroy.org%2FCdF%2F2019-2020%2F&amp\;data=05%7C01%7C
 Annie.Bacon%40newton.ac.uk%7C3a72cc5ee0a84105a47608da6982ad51%7C49a50445bd
 fa4b79ade3547b4f3986e9%7C0%7C0%7C637938307206974330%7CUnknown%7CTWFpbGZsb3
 d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C300
 0%7C%7C%7C&amp\;sdata=pcb4vRIMmGJFqzN5eD0e0cvJj2vidqyxMY54FP%2FFIGU%3D&amp
 \;reserved=0) that tries to show why and how interactive theorem proving i
 s increasingly used for P.L. research\, and to illustrate the approaches b
 y mechanizing in Coq most of Nielson and Nielson's textbook "Semantics wit
 h applications: an appetizer".&nbsp\; The course focuses on how to go from
  high-level intuitions and historical perspectives to the formal definitio
 ns and theorem statements\; how to conduct the proofs was barely mentioned
 .&nbsp\; I'll discuss what worked well and what worked not so well with th
 is approach.
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR