BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Formalisation of mathematics with interactive theo
 rem provers 
SUMMARY:Experiences with Isabelle/HOL: Formalising Real Al
 gebraic Geometry - Artie Khovanov (University of C
 ambridge)\, Michael Nedzelsky (Diffblue Ltd) and D
 r Wenda Li (University of Edinburgh)
DTSTART;TZID=Europe/London:20240222T170000
DTEND;TZID=Europe/London:20240222T180000
UID:TALK211648AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/211648
DESCRIPTION:The Isabelle/HOL interactive theorem prover has mu
 ltiple frameworks for formalising abstract algebra
 : one library which relies on typeclasses\, and an
 other\, better suited to formalising algebra\, whi
 ch makes no use of them. In this talk\, we discuss
  the experience of formalising material in real al
 gebraic geometry – real closed fields\, Thom encod
 ing and Puiseux series – in the latter framework. 
 We explore the strengths and weaknesses of the ava
 ilable automation\, as well as the feasibility of 
 transferring results from one library to the other
 .\n\n—-\n\nWATCH ONLINE HERE : https://www.microso
 ft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 
 Meeting ID: 370 771 279 261 Passcode: iCo7a5
LOCATION:MR14 Centre for Mathematical Sciences
CONTACT:Anand Rao Tadipatri
END:VEVENT
END:VCALENDAR