POPL 2018 (series) / CPP 2018 (series) / CPP 2018 - The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs /
A Constructive Formalisation of Semi-algebraic Sets and Functions
Tue 9 Jan 2018 15:00 - 15:30 at Museum A - Type Theory, Set Theory, and Formalized Mathematics Chair(s): Thorsten Altenkirch
Semi-algebraic sets and semi-algebraic functions are essential to specify and certify cylindrical algebraic decomposition algorithms. We formally define in Coq the base operations on semi-algebraic sets and functions using embedded first-order formulae over the language of real closed fields, and we prove the correctness of their geometrical interpretation. In doing so, we exploit a previous formalisation of quantifier elimination on such embedded formulae to guarantee the decidability of several first-order properties and keep our development constructive. We also exploit it to formalise formulae substitution without having to handle bound variables.
Tue 9 JanDisplayed time zone: Tijuana, Baja California change
Tue 9 Jan
Displayed time zone: Tijuana, Baja California change
13:30 - 15:30 | Type Theory, Set Theory, and Formalized MathematicsCPP at Museum A Chair(s): Thorsten Altenkirch University of Nottingham | ||
13:30 30mTalk | Finite Sets in Homotopy Type Theory CPP Dan Frumin Radboud University, Herman Geuvers Radboud University Nijmegen, Netherlands, Léon Gondelman LRI, Université Paris-Sud, Niels van der Weide Radboud University Nijmegen, Netherlands DOI | ||
14:00 30mTalk | Generic Derivation of Induction for Impredicative Encodings in Cedille CPP DOI | ||
14:30 30mTalk | Large Model Constructions for Second-Order ZF in Dependent Type Theory CPP DOI | ||
15:00 30mTalk | A Constructive Formalisation of Semi-algebraic Sets and Functions CPP Boris Djalal INRIA |