On Thursday 09/07/2009, at 11h, in room Fermat Jaune.
Speaker: Guillaume Allais.
Title: Towards a minimal axiom system for the reals numbers in Coq.
Abstract:
Guillaume Allais will present his internship work. The goal is to remove the axiom from Coq’s Reals library stating that: sin(pi/2)=1. The work requires the manipulation of real analysis concepts, in particular trigonometric functions and their properties.
