Thursday, June 16, 2016 - 11:30am to 12:30pm
Location:Blelloch-Skees Conference Room 8115 Gates & Hillman Centers
Speaker:OLIVIER HERMANT, Associate Researcher http://www.cri.ensmp.fr/people/hermant/
The λΠ-calculus modulo theory, implemented in the Dedukti system, is a logical framework where many theories can be expressed: constructive and classical predicate logic, Simple type theory, programming languages, Pure type systems, the Calculus of inductive constructions with universes... This allows to use it to check large libraries of proofs coming from various proofsystems: Zenon, iProver, FoCaLiZe, HOL-Light, and Matita.
Olivier Hermant is an associate researcher at MINES ParisTech, on a sabbatical leave at Wesleyan University. He got his PhD in 2005, under the supervision of Gilles Dowek, and his research interests are the combination of rewriting and proof systems, automated theorem proving, semantics and completeness theorems, and type systems.
Faculty Host: Robert Harper