BEGIN:VCALENDAR
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:
A formal set-theoretical model of Coq and its application to
strong normalization
STATUS:CONFIRMED
ATTENDEE;CN="Bruno Barras
":
MAILTO:no@spam.com
DESCRIPTION:
I will describe the formalization in Coq of two crucial met
atheoretical properties of the formalism of the Coq proof as
sistant: consistency and strong normalization (SN). While it
is clear why we prove the consistency of a logical formalis
m\, I will give a motivation for the SN property. Of course\
, as Gödel showed\, proving the consistency of a formalism i
n itself is only proving it is inconsistent. The usual way o
ut is to make Coq stronger by adding axioms. In our case\, w
e have extended Coq to make it as strong as intuitionistic s
et-theory with Grothendieck universes (an intuitionistic cou
nterpart of inaccessible cardinals). Then\, I will sketch an
intuitive translation from the Calculus of Inductive Constr
uctions (the formalism of Coq) to set theory\, and prove tha
t this interpretation is sound. The difficult part is to int
erpret inductive types. As a reward\, we derive the consiste
ncy of Coq relative to the set theory described above. Using
a slight variant of the set-theoretical interpretation\, I
will explain how to build a strong normalization model\, whi
ch soundness implies the SN property. The remarkable feature
of this model is that it is very modular: the complexity of
inductive types have been broken into simpler principles.
DTSTART;TZID=Europe/Paris:20170328T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201703281
100
UID:LSVsemLSV.201703281100@lsv.ens-cachan.fr
LOCATION:Auditorium Daniel Chemla (Bât. Institut D'Alembert)
END:VEVENT
END:VCALENDAR