Chantal Keller

29 papers A* 1A 1B 9Journal 5Unranked 10
YearRankTypeTitle / Venue / Authors
2025 B ed.
16th International Conference on Interactive Theorem Proving, ITP 2025, Reykjavik, Iceland, September 28 - October 1, 2025
ITP
Yannick Forster, Chantal Keller
2023 B conf
An Interactive SMT Tactic in Coq using Abductive Reasoning.
LPAR
Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett
2023 B conf
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory.
CPP
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial
2022 J jnl
Modular pre-processing for automated reasoning in dependent type theory.
CoRR
Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial
2022 J jnl
Translating Canonical SQL to Imperative Code in Coq.
CoRR
Véronique Benzaken, Evelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, Jérôme Siméon
2022 J jnl
Translating canonical SQL to imperative code in Coq.
Proc. ACM Program. Lang.
Véronique Benzaken, Evelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, Jérôme Siméon
2021 B conf
A Coq formalization of data provenance.
CPP
Véronique Benzaken, Sarah Cohen-Boulakia, Evelyne Contejean, Chantal Keller, Rébecca Zucchini
2021 — conf
General Automation in Coq through Modular Transformations.
PxTP
Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial
2021 — ed.
Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021.
PxTP
Chantal Keller, Mathias Fleury
2020 — conf
On the Semantics of Polychronous Polytimed Specifications.
FORMATS
Hai Nguyen Van, Thibaut Balabonski, Frédéric Boulanger, Chantal Keller, Benoît Valiron, Burkhart Wolff
2019 — ed.
Tests and Proofs - 13th International Conference, TAP@FM 2019, Porto, Portugal, October 9-11, 2019, Proceedings
TAP@FM
Dirk Beyer, Chantal Keller
2018 B conf
A Coq Formalisation of SQL's Execution Engines.
ITP
Véronique Benzaken, Evelyne Contejean, Chantal Keller, Eunice Martins
2018 — conf
Tactic Program-Based Testing and Bounded Verification in Isabelle/HOL.
TAP@STAF
Chantal Keller
2017 — conf
A Symbolic Operational Semantics for TESL - With an Application to Heterogeneous System Testing.
FORMATS
Hai Nguyen Van, Thibaut Balabonski, Frédéric Boulanger, Chantal Keller, Benoît Valiron, Burkhart Wolff
2017 — conf
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq.
CAV (2)
Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett
2016 A conf
A Certified Compiler for Verifiable Computing.
CSF
Cédric Fournet, Chantal Keller, Vincent Laporte
2016 A* conf
Dependent types and multi-monadic effects in F.
POPL
Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, Santiago Zanella-Béguelin
2016 — conf
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract).
HaTT@IJCAR
Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds, Cesare Tinelli
2014 — conf
Beagle as a HOL4 external ATP method.
PAAR@IJCAR
Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish
2014 — conf
Typeful Normalization by Evaluation.
TYPES
Olivier Danvy, Chantal Keller, Matthias Puech
2013 — —
A Matter of Trust: Skeptical Communication Between Coq and External Provers. (Question de confiance : communication sceptique entre Coq et des prouveurs externes).
Chantal Keller
2013 — conf
Extended Resolution as Certificates for Propositional Logic.
PxTP@CADE
Chantal Keller
2012 J jnl
Parametricity in an Impredicative Sort
CoRR
Chantal Keller, Marc Lasson
2012 B conf
Parametricity in an Impredicative Sort.
CSL
Chantal Keller, Marc Lasson
2012 B conf
Pseudo-Weight: Making Tabletop Interaction with Virtual Objects More Tangible.
ITS
Chantal Keller, Jérémy Bluteau, Renaud Blanch, Sabine Coquillart
2012 J jnl
The Refined Calculus of Inductive Construction: Parametricity and Abstraction
CoRR
Chantal Keller, Marc Lasson
2011 B conf
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses.
CPP
Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner
2010 — conf
Hereditary Substitutions for Simple Types, Formalized.
MSFP@ICFP
Chantal Keller, Thorsten Altenkirch
2010 B conf
Importing HOL Light into Coq.
ITP
Chantal Keller, Benjamin Werner