General Automation in Coq through Modular Transformations

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

Type: Paratext

Publication Date: 2021-07-11

Citations: 0

Locations

Electronic Proceedings in Theoretical Computer Science - View
arXiv (Cornell University) - View - PDF
Lirias (KU Leuven) - View - PDF
HAL (Le Centre pour la Communication Scientifique Directe) - View - PDF

Similar Works

Action	Title	Year	Authors
+ PDF Chat	General Automation in Coq through Modular Transformations	2021	Valentin Blot Louise Dubois de Prisque Chantal Keller Pierre Vial
+ PDF Chat	Compositional Pre-processing for Automated Reasoning in Dependent Type Theory	2023	Valentin Blot Denis Cousineau Enzo Crance Louise Dubois de Prisque Chantal Keller Assia Mahboubi Pierre Vial
+	Compositional pre-processing for automated reasoning in dependent type theory	2022	Valentin Blot Denis Cousineau Enzo Crance Louise Dubois de Prisque Chantal Keller Assia Mahboubi Pierre Vial
+ PDF Chat	Towards Automatic Transformations of Coq Proof Scripts	2024	Nicolas Magaud
+	Towards Proof Repair in Cubical Agda	2023	Cosmo Viola Max Fan Talia Ringer
+	The Multiverse: Logical Modularity for Proof Assistants	2021	Kenji Maillard Nicolas Margulies Matthieu Sozeau Nicolas Tabareau Éric Tanter
+	Martin-Löf à la Coq	2023	Arthur Adjedj Meven Lennon-Bertrand Kenji Maillard Pierre-Marie Pédrot Loïc Pujet
+	Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant	2015	Théo Zimmermann Hugo Herbelin
+	Reliably Reproducing Machine-Checked Proofs with the Coq Platform	2022	Karl Palmskog E. ̃Tassi Théo Zimmermann
+ PDF Chat	Trocq: Proof Transfer for Free, With or Without Univalence	2024	Cyril Cohen Enzo Crance Assia Mahboubi
+ PDF Chat	Touring the MetaCoq Project (Invited Paper)	2021	Matthieu Sozeau
+	Coqatoo: Generating Natural Language Versions of Coq Proofs	2017	Andrew Bedford
+ PDF Chat	Touring the MetaCoq Project (Invited Paper)	2021	Matthieu Sozeau
+ PDF Chat	Proust: A Nano Proof Assistant	2016	Prabhakar Ragde
+	From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures	2008	Frédéric Blanqui Jean-Pierre Jouannaud Pierre-Yves Strub
+	MirrorShard: Proof by Computational Reflection with Verified Hints	2013	Gregory Malecha Adam Chlipala Thomas Braibant Patrick Hulin Edward Z. Yang
+	Comparison of Two Theorem Provers: Isabelle/HOL and Coq	2018	Artem Yushkovskiy
+	A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory	2023	Reynald Affeldt Jacques Garrigue Takafumi Saikawa
+ PDF Chat	Verified and Optimized Implementation of Orthologic Proof Search	2025	Simon Guilloud Clément Pit-Claudel
+ PDF Chat	Extending Nunchaku to Dependent Type Theory	2016	Simon Cruanes Jasmin Christian Blanchette

Works That Cite This (0)

Action	Title	Year	Authors

Works Cited by This (1)

Action	Title	Year	Authors
+ PDF Chat	Encoding Monomorphic and Polymorphic Types	2017	Jasmin Christian Blanchette Sascha Böhme Andrei Popescu Nicholas Smallbone