BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Matryoshka: Extending Superposition Provers and SMT Solvers to Hig
 her-Order Logic
DTSTART:20190403T140000
DTEND:20190403T153000
DTSTAMP:20260413T140727Z
UID:5e59212c07d017465b35e73e0f4e4ec3eeedccff04dbba744652c18c
CATEGORIES:Conferences - Seminars
DESCRIPTION:by Jasmin Christian Blanchette\n\nAbstract\nThe Matryoshka pro
 ject [*] aims at reducing the gap between the logics of automatic and inte
 ractive theorem provers. Our approach is to enrich the two leading approac
 hes for first-order reasoning\, namely superposition and SMT\, with higher
 -order reasoning in a careful manner\, to preserve their performance and a
 ny completeness guarantees. We initially focused on supporting currying (a
 pplied variables and partial application) and have now started investigati
 ng lambdas and higher-order unification\, with promising results. Our tech
 niques are implemented in the superposition-based provers Zipperposition a
 nd E and the SMT solvers veriT and CVC4.\n\nBio\nJasmin Christian Blanchet
 te is an assistant professor in the Theoretical Computer Science section o
 f the Vrije Universiteit Amsterdam\, in the Netherlands. He is also a gues
 t researcher in the VeriDis group at Loria in Nancy\, France\, and in the 
 Automation of Logic group at the Max-Planck-Institut für Informatik in Sa
 arbrücken\, Germany. He was a postdoc at the Chair for Logic and Verifica
 tion at the Technische Universität München\, Germany\, which he joined i
 n 2008 as a PhD student. From 2000 to 2008\, he worked as software enginee
 r and documentation manager for Trolltech (now The Qt Company) in Oslo\, N
 orway.\nHis research focuses on the use of first-order automatic theorem p
 rovers and model finders to find proofs and counterexamples in higher-orde
 r logic (Sledgehammer\, Nitpick\, Nunchaku\, and Matryoshka). Another aspe
 ct of his work is the development of foundational definitional mechanisms 
 for (co)datatypes and (co)recursive functions. He is also interested in fo
 rmalizing classic results and modern research in automated reasoning (IsaF
 oL) and number theory (Lean Forward).\n\nMore information
LOCATION:BC 410 https://plan.epfl.ch/?room==BC%20410
STATUS:CANCELLED
END:VEVENT
END:VCALENDAR