Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Sun 17 Jan 2021 19:00 - 19:15 at CPP - Formalized Mathematics Chair(s): Amin Timany

Semi-algebraic sets and real analytic functions are fundamental concepts in Real Algebraic Geometry and Real Analysis, respectively. These concepts interact in the study of Differential Equations, where the real analytic solution to a differential equation is known to enter or exit a semi-algebraic set in a predicable way. Motivated to enhance the capability to reason about differential equations in the Prototype Verification System (PVS), a formalization of multivariate polynomials, semi-algebraic sets, and real analytic functions is developed. The favorable way that a real analytic function enters and exits a semi-algebraic set is proven. It is further shown that if the function is assumed to be smooth, a slightly weaker assumption than real analytic, these favorable interactions with semi-algebraic sets may fail.

Sun 17 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:45 - 19:30
Formalized MathematicsCPP at CPP
Chair(s): Amin Timany Aarhus University

Streamed session: https://youtu.be/U_ZT9hfDAUQ?t=2768

18:45
15m
Talk
Formalizing the Ring of Witt VectorsDistinguished Paper Award
CPP
Johan Commelin Universität Freiburg, Robert Y. Lewis Vrije Universiteit Amsterdam
Pre-print Media Attached
19:00
15m
Talk
Formal Verification of Semi-algebraic Sets and Real Analytic Functions
CPP
J Tanner Slagel NASA Langley Research Center, Lauren White Kansas State University, Aaron Dutle NASA Langley Research Center
Pre-print Media Attached
19:15
15m
Talk
On the Formalisation of Kolmogorov Complexity
CPP
Elliot Catt ANU, Michael Norrish Data61, CSIRO & ANU
Pre-print Media Attached