Home
EPiC Series
Kalpa Publications
Preprints
For Authors
For Editors
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
Copyright © 2012-2023 easychair.org. All rights reserved.