BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:[CANCELLED] Real Closed Field and Thom Encoding in Isabelle/HOL   
 - Dr Wenda Li (University of Cambridge)\, Artem Khovanov (University of Ca
 mbridge) and Michael Nedzelsky (Diffblue Ltd)
DTSTART:20230309T170000Z
DTEND:20230309T180000Z
UID:TALK193720@talks.cam.ac.uk
CONTACT:Angeliki Koutsoukou-Argyraki
DESCRIPTION:Real closed fields (RCFs) are fields that share many of the sa
 me algebraic properties as the field of real numbers. One notable example 
 of RCF is the field of real algebraic numbers\, which can be finitely enco
 ded (e.g.\, as an integer polynomial and a rational interval) and effectiv
 ely computed. However\, RCFs also include non-Archimedean examples\, which
  are fields extended with infinitesimals. Computing numbers on these field
 s may require using Thom encoding to distinguish polynomial roots with inf
 initesimal coefficients. In this talk\, we will discuss a formalisation of
  real closed field and Thom encoding in the Isabelle proof assistant. We w
 ill also share our experience of utilising the types-to-sets framework in 
 an ongoing proof that demonstrates the equivalence between different defin
 itions of RCFs.
LOCATION:  Centre for Mathematical Sciences MR12\, CMS
END:VEVENT
END:VCALENDAR