University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > [CANCELLED] Real Closed Field and Thom Encoding in Isabelle/HOL

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

[CANCELLED] Real Closed Field and Thom Encoding in Isabelle/HOL

Download to your calendar using vCal

If you have a question about this talk, please contact Angeliki Koutsoukou-Argyraki .

[CANCELLED, please check back for rescheduling]

Real closed fields (RCFs) are fields that share many of the same algebraic properties as the field of real numbers. One notable example of RCF is the field of real algebraic numbers, which can be finitely encoded (e.g., as an integer polynomial and a rational interval) and effectively computed. However, RCFs also include non-Archimedean examples, which are fields extended with infinitesimals. Computing numbers on these fields may require using Thom encoding to distinguish polynomial roots with infinitesimal coefficients. In this talk, we will discuss a formalisation of real closed field and Thom encoding in the Isabelle proof assistant. We will also share our experience of utilising the types-to-sets framework in an ongoing proof that demonstrates the equivalence between different definitions of RCFs.

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Hybrid: Seminar room, SPRI & Zoom - email organiser for details Cambridge University Engineering Department, LR2 Webinar & LT2, Computer Laboratory, William Gates Building.

Other talks

Title to be confirmed Coming soon Scientific Steering Committee meeting Ensemble inequivalence for systems with long-range interactions Title to be confirmed Title to be confirmed
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity