Assisted and Automated Theorem Proving
Event details
| Date | 01.07.2016 |
| Hour | 13:00 › 15:00 |
| Speaker | Romain Edelmann |
| Location | |
| Category | Conferences - Seminars |
EDIC Candidacy Exam
Exam President: Prof. Willy Zwaenepoel
Thesis Director: Prof. Viktor Kuncak
Co-examiner: Prof. Martin Odersky
Background papers:
Dependent Types and Multi-monadic Effects in F⋆
Decision Procedures for Algebraic Data Types with Abstractions.
MaLARea SG1-Machine Learner for Automated Reasoning with Semantic Guidance
Abstract:
In this paper, we survey three papers related to programming language design, automated verification tools and automated theorem proving. The first paper describes the design of F*, a dependently typed language with an effect system. The second describes a decision procedure to verify functional programs consisting of algebraic data types with fold abstraction functions. The last paper presents a machine learning system incorporating semantic relevance concepts to automatically prove conjectures in large mathematical theories. While coming from different areas, all those papers offer some insights which can potentially be applied to the Leon verification tool.
Exam President: Prof. Willy Zwaenepoel
Thesis Director: Prof. Viktor Kuncak
Co-examiner: Prof. Martin Odersky
Background papers:
Dependent Types and Multi-monadic Effects in F⋆
Decision Procedures for Algebraic Data Types with Abstractions.
MaLARea SG1-Machine Learner for Automated Reasoning with Semantic Guidance
Abstract:
In this paper, we survey three papers related to programming language design, automated verification tools and automated theorem proving. The first paper describes the design of F*, a dependently typed language with an effect system. The second describes a decision procedure to verify functional programs consisting of algebraic data types with fold abstraction functions. The last paper presents a machine learning system incorporating semantic relevance concepts to automatically prove conjectures in large mathematical theories. While coming from different areas, all those papers offer some insights which can potentially be applied to the Leon verification tool.
Practical information
- General public
- Free
Contact
- Cecilia Chapuis EDIC