Chantal Keller is a Lecturer in the Computer Science Department at IUT d'Orsay, University of Paris-Saclay, and a member of the Laboratoire Méthodes Formelles (LMF), a joint research unit involving CNRS, ÉNS Paris-Saclay, and Inria. Her research lies at the intersection of programming language theory and formal methods, with a focus on type theory, interactive theorem proving, and the integration of automated and interactive provers. Her primary research interests include formal verification , type theory , Coq , SMT solvers , program testing , and data-centric applications . She is particularly known for her development of SMTCoq , an interface that enables Coq to verify results from external SAT and SMT solvers, enhancing trust in automated reasoning. She has also contributed to tools such as HOL-TestGen and DataCert , and has formalized SQL execution engines and data provenance. Her recent publications span topics such as formal semantics of timed systems, certified compilation, cryptographic verification, and normalization by evaluation. These works reflect a strong emphasis on certified software , proof automation , and deep specifications . A Matter of Trust: Skeptical Communication Between Coq and External Provers (PhD Thesis, 2013) Member, POPL External Review Committee (2017) Program Committee Member, CPP, ITP, TAP, SMT, JFLA, CoqPL, and others Co-PC Chair, ITP (2025) Coordinator, Digicosme UPSCaLe working group (2017–2022) Keller actively contributes to the academic community through program committee memberships and organizing roles. She has advised research projects and mentored students, though no formal PhD advisees are listed. Her work bridges theoretical foundations with practical applications in security and database systems. She has no explicitly listed scientific awards, but her sustained contributions to formal methods and theorem proving indicate significant recognition in her field.
