7 citations · 14 across the 6 of their papers we have counts for
7 papers
Compositional pre-processing for automated reasoning in dependent type theory
Valentin Blot, Denis Cousineau, Enzo Crance +4
In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited…
Translating Canonical SQL to Imperative Code in Coq
Véronique Benzaken, Évelyne Contejean, Mohammed Houssem Hachmaoui +4
SQL is by far the most widely used and implemented query language. Yet, on some key features, such as correlated queries and NULL value semantics, many implementations diverge or c…
General Automation in Coq through Modular Transformations
Valentin Blot, Louise Dubois de Prisque, Chantal Keller +1
Whereas proof assistants based on Higher-Order Logic benefit from external solvers' automation, those based on Type Theory resist automation and thus require more expertise. Indeed…
Proceedings Seventh Workshop on Proof eXchange for Theorem Proving
Chantal Keller, Mathias Fleury
This volume of EPTCS contains the proceedings of the Seventh Workshop on Proof Exchange for Theorem Proving (PxTP 2021), held on 11 July 2021 as part of the CADE-28 online conferen…
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)
Burak Ekici, Guy Katz, Chantal Keller +3
This extended abstract reports on current progress of SMTCoq, a communication tool between the Coq proof assistant and external SAT and SMT solvers. Based on a checker for generic…
The Refined Calculus of Inductive Construction: Parametricity and Abstraction
Chantal Keller, Marc Lasson
We present a refinement of the Calculus of Inductive Constructions in which one can easily define a notion of relational parametricity. It provides a new way to automate proofs in…