Keyword:Coq

Publications
Quasi Morphisms for Almost Full Relations Dominique Larchey-Wendling EasyChair Preprint 13175
Hemiola: a DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols Joonwon Choi, Adam Chlipala and Arvind EasyChair Preprint 8623
Towards Corecursion Without Corecursion in Coq Vlad Rusu and David Nowak EasyChair Preprint 8442
A type-theoretical reduction of morphological, syntactic and semantic compositionality to a single level of description Erkki Luuk EasyChair Preprint 1516
A Coq mechanised formal semantics for realistic SQL queries : Formally reconciling SQL and (extended) relational algebra. Véronique Benzaken and Évelyne Contejean EasyChair Preprint 472
Certification of Tail Recursive Bubble--Sort in Theorema and Coq Isabela Dramnesc, Tudor Jebelean and Sorin Stratulat In:LPAR 2024 Complementary Volume
An Interactive SMT Tactic in Coq using Abductive Reasoning Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli and Clark Barrett In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Tactic Learning and Proving for the Coq Proof Assistant Lasse Blaauwbroek, Josef Urban and Herman Geuvers In:LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
A Verified Theorem Prover Backend Supported by a Monotonic Library Vincent Rahli, Liron Cohen and Mark Bickford In:LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Coq without Type Casts: A Complete Proof of Coq Modulo Theory Jean-Pierre Jouannaud and Pierre-Yves Strub In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
From Tarski to Descartes: Formalization of the Arithmetization of Euclidean Geometry Pierre Boutry, Gabriel Braun and Julien Narboux In:SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science
Towards Verified Construction for Planar Class of a Qualitative Spatial Representation Sosuke Moriguchi, Mizuki Goto and Kazuko Takahashi In:SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science
Verification of a brick Wang tiling algorithm Toshiaki Matsushima, Yoshihiro Mizoguchi and Alexandre Derouet-Jourdan In:SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science
Machine Learning of Coq Proof Guidance: First Experiments Cezary Kaliszyk, Lionel Mamane and Josef Urban In:SCSS 2014. 6th International Symposium on Symbolic Computation in Software Science
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs Nada Habli and Amy P. Felty In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving