BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Assisted and Automated Theorem Proving
DTSTART:20160701T130000
DTEND:20160701T150000
DTSTAMP:20260407T024729Z
UID:5b55e362dbddc208f8a254fd228254e3189bbbfa0241aeb086b9f4c8
CATEGORIES:Conferences - Seminars
DESCRIPTION:Romain Edelmann\nEDIC Candidacy Exam\nExam President: Prof. Wi
 lly Zwaenepoel\nThesis Director: Prof. Viktor Kuncak\nCo-examiner: Prof. M
 artin Odersky\nBackground papers:Dependent Types and Multi-monadic Effects
  in F⋆Decision Procedures for Algebraic Data Types with Abstractions.MaL
 ARea SG1-Machine Learner for Automated Reasoning with Semantic GuidanceAbs
 tract:\nIn this paper\, we survey three papers related to programming lang
 uage 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 abstract
 ion functions. The last paper presents a machine learning system incorpora
 ting semantic relevance concepts to automatically prove conjectures in lar
 ge mathematical theories. While coming from different areas\, all those pa
 pers offer some insights which can potentially be applied to the Leon veri
 fication tool.
LOCATION:BC 129 https://plan.epfl.ch/?room==BC%20129
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR