Chantal Keller

According to our database, Chantal Keller authored at least 24 papers between 2010 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2023

An Interactive SMT Tactic in Coq using Abductive Reasoning.

Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark W. Barrett

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

Compositional Pre-processing for Automated Reasoning in Dependent Type Theory.

Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

2022

Translating canonical SQL to imperative code in Coq.

Véronique Benzaken, Evelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, Jérôme Siméon

Proc. ACM Program. Lang., 2022

Modular pre-processing for automated reasoning in dependent type theory.

Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial

CoRR, 2022

2021

General Automation in Coq through Modular Transformations.

Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial

Proceedings of the Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, 2021

A Coq formalization of data provenance.

Véronique Benzaken, Sarah Cohen-Boulakia, Evelyne Contejean, Chantal Keller, Rébecca Zucchini

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2020

On the Semantics of Polychronous Polytimed Specifications.

Hai Nguyen Van, Thibaut Balabonski, Frédéric Boulanger, Chantal Keller, Benoît Valiron, Burkhart Wolff

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2020

2018

Tactic Program-Based Testing and Bounded Verification in Isabelle/HOL.

Chantal Keller

Proceedings of the Tests and Proofs - 12th International Conference, 2018

A Coq Formalisation of SQL's Execution Engines.

Véronique Benzaken, Evelyne Contejean, Chantal Keller, Eunice Martins

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017

A Symbolic Operational Semantics for TESL - With an Application to Heterogeneous System Testing.

Hai Nguyen Van, Thibaut Balabonski, Frédéric Boulanger, Chantal Keller, Benoît Valiron, Burkhart Wolff

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2017

SMTCoq: A Plug-In for Integrating SMT Solvers into Coq.

Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016

Extending SMTCoq, a Certified Checker for SMT (Extended Abstract).

Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds, Cesare Tinelli

Proceedings of the Proceedings First International Workshop on Hammers for Type Theories, 2016

Dependent types and multi-monadic effects in F.

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

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

A Certified Compiler for Verifiable Computing.

Cédric Fournet, Chantal Keller, Vincent Laporte

Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

2014

Typeful Normalization by Evaluation.

Olivier Danvy, Chantal Keller, Matthias Puech

Proceedings of the 20th International Conference on Types for Proofs and Programs, 2014

Beagle as a HOL4 external ATP method.

Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish

Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

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

PhD thesis, 2013

Extended Resolution as Certificates for Propositional Logic.

Chantal Keller

Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

2012

The Refined Calculus of Inductive Construction: Parametricity and Abstraction

Chantal Keller, Marc Lasson

CoRR, 2012

Pseudo-Weight: Making Tabletop Interaction with Virtual Objects More Tangible.

Chantal Keller, Jérémy Bluteau, Renaud Blanch, Sabine Coquillart

Proceedings of the Interactive Tabletops and Surfaces, 2012

Parametricity in an Impredicative Sort.

Chantal Keller, Marc Lasson

Proceedings of the Computer Science Logic (CSL'12), 2012

2011

A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses.

Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

Importing HOL Light into Coq.

Chantal Keller, Benjamin Werner

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Hereditary Substitutions for Simple Types, Formalized.

Chantal Keller, Thorsten Altenkirch

Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, 2010