Français English
Research
My main research topics are:
- Type Theory
- implementation and use of interactive theorem provers (in
particular Coq, Agda, HOL
Light) and automatic theorem provers (notably SAT and
SMT solvers)
- cooperation between provers
- the parametricity theory and its applications
In particular, I develop:
-
an interface to call external SMT solvers in Coq without
compromising soundness: SMTCoq
-
a "theorems for free" generator in Coq based on parametricity: CoqParam
-
an interface to import and check HOL-Light's theorems in
Coq: HOLLIGHTCOQ
In 2013, I am a member of the program committee of the
workshop Proof Exchange for Theorem
Proving.
Below is a list of my publications and
some talks.
Publications
Conferences and workshops with proceedings
-
Parametricity in an Impredicative Sort,
Keller, Chantal; Lasson, Marc,
CSL - 26th International
Workshop/21st Annual Conference of the EACSL -
2012. PDF,
PS, BIBTEX
-
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses,
Armand, Michaël; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Thery, Laurent; Werner, Benjamin,
CPP - Certified Programs and Proofs
- First International Conference -
2011. PDF, BIBTEX
-
Verifying SAT and SMT in Coq for a fully automated decision procedure,
Armand, Mickaël; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Théry, Laurent; Wener, Benjamin,
PSATTT - International Workshop on Proof-Search in Axiomatic
Theories and Type Theories - 2011. PDF, BIBTEX
-
Hereditary Substitutions for Simple Types, Formalized,
Keller, Chantal; Altenkirch, Thorsten,
MSFP - Third Workshop on
Mathematically Structured Functional Programming -
2010. PDF, BIBTEX
-
Importing HOL Light into Coq,
Keller, Chantal; Werner, Benjamin,
ITP -
Interactive Theorem Proving, First International Conference -
2010. PDF, BIBTEX
Conferences and workshops without proceedings
-
The Refined Calculus of Inductive Construction: Parametricity and Abstraction,
Keller, Chantal; Lasson, Marc,
LICS - 27th Annual
IEEE Symposium on Logic in Computer Science -
2012. PDF,
PS, BIBTEX
Internship reports
-
Importation de
preuves HOL Light en Coq (in French), master internship under
the supervision of Benjamin
Werner in the
INRIA TypiCal team
of Laboratoire
d'Informatique de
Polytechnique - 2009. PDF, BIBTEX
-
Substitutions for
simply-typed λ-calculus, master internship under the supervision
of Thorsten
Altenkirch in the Functional Programming team of the
School of Computer
Science at the
University of
Nottingham - 2008. PDF, BIBTEX
-
Manipulation
pseudo-haptique d'entités 2D (in French), licence internship
under the supervision
of Sabine
Coquillart and Renaud
Blanch at INRIA
Rhône-Alpes and Laboratoire
d'Informatique de
Grenoble - 2007. PDF, BIBTEX
Unpublished notes
-
The
category of simply typed λ-terms in Agda, Keller, Chantal. PDF, BIBTEX
Top of the page
Talks
International conferences
-
Parametricity in
an Impredicative Sort. CSL
2012
-
A Modular Integration of SAT/SMT Solvers to Coq through Proof
Witnesses. CPP
2011
-
Importing
HOL Light into
Coq. ITP 2010
-
Hereditary
Substitutions for Simple Types, Formalized. MSFP 2010
Meetings, seminars
-
Encoding HOL
into
Dedukti. CORIAS
meeting on 11/2/10
-
Coopération entre
prouveurs SAT, SMT et
Coq (in
French). LAC
meeting on November 2010
-
Importation
de HOL Light dans
Coq (in
French). GEOCAL-LAC
meeting on March 2010
Miscellaneous
-
Presentation of the
TypiCal team. Transverse seminar on computer-aided deduction.
Top of the page
Last update: 03/19/13