LISA : A Formal Theorem Prover Using Set Theory
Event details
| Date | 02.07.2021 |
| Hour | 13:00 › 15:00 |
| Speaker | Simon Guilloud |
| Category | Conferences - Seminars |
EDIC candidacy exam
exam president: Prof. Christoph Koch
thesis advisor: Prof. Viktor Kuncak
co-examiner: Prof. Jacques Duparc
Abstract
I will work on the design and implementation of a new foundational system for formal theorem proving and formal program verification. The project first involves the implementation of first order logic 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 this kernel will then be built an actual theorem proving environment, automation tools, a programming language whose semantic will be formalized in the underlying system and finally the basis of a mathematical library of theorems. Compared to already existing (successful but old) theorem provers, we expect our work to be relevant for multiple reasons. In particular, we want our system to be closer to the mathematical education of scientists and engineers and to facilitate formal verification of programs. We also aim for use and inclusion of modern results. For example, we work on efficient structures and algorithm to check formula equivalence for a large class equivalence, including Associative-Commutative operations, alpha-equivalence and other normal forms.
Background papers
exam president: Prof. Christoph Koch
thesis advisor: Prof. Viktor Kuncak
co-examiner: Prof. Jacques Duparc
Abstract
I will work on the design and implementation of a new foundational system for formal theorem proving and formal program verification. The project first involves the implementation of first order logic 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 this kernel will then be built an actual theorem proving environment, automation tools, a programming language whose semantic will be formalized in the underlying system and finally the basis of a mathematical library of theorems. Compared to already existing (successful but old) theorem provers, we expect our work to be relevant for multiple reasons. In particular, we want our system to be closer to the mathematical education of scientists and engineers and to facilitate formal verification of programs. We also aim for use and inclusion of modern results. For example, we work on efficient structures and algorithm to check formula equivalence for a large class equivalence, including Associative-Commutative operations, alpha-equivalence and other normal forms.
Background papers
- Maziarz, Krzysztof, Tom Ellis, Alan Lawrence, Andrew Fitzgibbon, et Simon Peyton Jones. « Hashing Modulo Alpha-Equivalence », 2021, 17. PLDI (2021), https://arxiv.org/abs/2105.02856
- Paulson, LawrenceC., et Krzysztof Grabczewski. « Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice ». Journal of Automated Reasoning 17, no 3 (December 1996). https://doi.org/10.1007/BF00283132.
- Werner, Benjamin. « Sets in Types, Types in Sets ». In Theoretical Aspects of Computer Software, edited by Martín Abadi and Takayasu Ito, 1281:530‑46. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg, 1997. https://doi.org/10.1007/BFb0014566.$
Practical information
- General public
- Free