Keyword:Coq

Papers
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
Towards Corecursion Without Corecursion in Coq Vlad Rusu and David Nowak EasyChair Preprint no. 8442
Hemiola: a DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols Joonwon Choi, Adam Chlipala and Arvind EasyChair Preprint no. 8623
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 type-theoretical reduction of morphological, syntactic and semantic compositionality to a single level of description Erkki Luuk EasyChair Preprint no. 1516
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
A Coq mechanised formal semantics for realistic SQL queries : Formally reconciling SQL and (extended) relational algebra. Véronique Benzaken and Évelyne Contejean EasyChair Preprint no. 472
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
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
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
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
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 Felty In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving