BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:LISA : A Formal Theorem Prover Using Set Theory
DTSTART:20210702T130000
DTEND:20210702T150000
DTSTAMP:20260501T210517Z
UID:dcddf7a5d224e876c61414e6d72e48e9a9e0db752fb7ec5929fe4e32
CATEGORIES:Conferences - Seminars
DESCRIPTION:Simon Guilloud\nEDIC candidacy exam\nexam president: Prof. Chr
 istoph Koch\nthesis advisor: Prof. Viktor Kuncak\nco-examiner: Prof. Jacqu
 es Duparc\n\nAbstract\nI will work on the design and implementation of a n
 ew foundational system for formal theorem proving and formal program verif
 ication. The project first involves the implementation of first order logi
 c and sequent calculus in a proof system that needs to be at the same time
  expressive\, practical and sufficiently small to be trusted. On top of th
 is kernel will then be built an actual theorem proving environment\,  aut
 omation tools\, a programming language whose semantic will be formalized i
 n the underlying system and finally the basis of a mathematical library of
  theorems. Compared to already existing (successful but old) theorem prove
 rs\, we expect our work to be relevant for multiple reasons. In particular
 \, we want our system to be closer to the mathematical education of scient
 ists and engineers and to facilitate formal verification of programs. We a
 lso aim for use and inclusion of modern results. For example\, we work on 
 efficient structures and algorithm to check formula equivalence for a larg
 e class equivalence\, including Associative-Commutative operations\, alpha
 -equivalence and other normal forms.\n\nBackground papers\n\n	Maziarz\, Kr
 zysztof\, Tom Ellis\, Alan Lawrence\, Andrew Fitzgibbon\, et Simon Peyton 
 Jones. « Hashing Modulo Alpha-Equivalence »\, 2021\, 17. PLDI (2021)\,
  https://arxiv.org/abs/2105.02856\n	Paulson\, LawrenceC.\, et Krzysztof Gr
 abczewski. « Mechanizing Set Theory: Cardinal Arithmetic and the Axiom o
 f Choice ». Journal of Automated Reasoning 17\, no 3 (December 1996). ht
 tps://doi.org/10.1007/BF00283132.\n	Werner\, Benjamin. « Sets in Types\,
  Types in Sets ». In Theoretical Aspects of Computer Software\, edited b
 y Martín Abadi and Takayasu Ito\, 1281:530‑46. Lecture Notes in Compute
 r Science. Berlin\, Heidelberg: Springer Berlin Heidelberg\, 1997. https:/
 /doi.org/10.1007/BFb0014566.$\n\n\n 
LOCATION:
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR