Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
16 | Daniel Ricketts 0001 |
Verification of Sampled-Data Systems using Coq. |
|
2017 |
RDF |
|
16 | Izumi Asakura, Hidehiko Masuhara, Tomoyuki Aotani |
Proof of Soundness of Concurrent Separation Logic for GPGPU in Coq. |
J. Inf. Process. |
2016 |
DBLP DOI BibTeX RDF |
|
16 | José Grimm |
Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers. |
J. Formaliz. Reason. |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Christoph-Simon Senjak, Martin Hofmann 0001 |
An implementation of Deflate in Coq. |
CoRR |
2016 |
DBLP BibTeX RDF |
|
16 | Jacques D. Fleuriot, Steven Obua, Phil Scott |
Social Network Processes in the Isabelle and Coq Theorem Proving Communities. |
CoRR |
2016 |
DBLP BibTeX RDF |
|
16 | Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, Vincent Siles |
Formalized linear algebra over Elementary Divisor Rings in Coq. |
Log. Methods Comput. Sci. |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters |
The HoTT Library: A formalization of homotopy type theory in Coq. |
CoRR |
2016 |
DBLP BibTeX RDF |
|
16 | François Clément, Vincent Martin |
The Lax-Milgram Theorem. A detailed proof to be formalized in Coq. |
CoRR |
2016 |
DBLP BibTeX RDF |
|
16 | Fabian Kunze |
Towards the Integration of an Intuitionistic First-Order Prover into Coq. |
HaTT@IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Lukasz Czajka 0001, Cezary Kaliszyk |
Goal Translation for a Hammer for Coq (Extended Abstract). |
HaTT@IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Allyx Fontaine, Akka Zemmari |
RDA: A Coq Library to Reason about Randomised Distributed Algorithms in the Message Passing Model. |
Sci. Ann. Comput. Sci. |
2016 |
DBLP BibTeX RDF |
|
16 | Érik Martin-Dorel, Guillaume Melquiond |
Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. |
J. Autom. Reason. |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Théo Zimmermann |
Design and development of a tool based on Coq to write and format mathematical proofs. |
FM4M/MathUI/ThEdu/DP/WIP@CIKM |
2016 |
DBLP BibTeX RDF |
|
16 | Allyx Fontaine, Akka Zemmari |
Certified Impossibility Results and Analyses in Coq of Some Randomised Distributed Algorithms. |
ICTAC |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Christoph-Simon Senjak, Martin Hofmann 0001 |
An Implementation of Deflate in Coq. |
FM |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Robbert Krebbers, Louis Parlant, Alexandra Silva 0001 |
Moessner's Theorem: An Exercise in Coinductive Reasoning in Coq. |
Theory and Practice of Formal Methods |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Lin Qian, Zhenhua Duan, Nan Zhang 0001, Cong Tian |
A Proof System for MSVL Programs in Coq. |
SOFL+MSVL |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Jacek Chrzaszcz, Aleksy Schubert, Jakub Zakrzewski 0001 |
Coq Support in HAHA. |
TYPES |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Philip Johnson-Freyd, Geoffrey C. Hulette, Zena M. Ariola |
Verification by Way of Refinement: A Case Study in the Use of Coq and TLA in the Design of a Safety Critical System. |
FMICS-AVoCS |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Wouter Swierstra, João Alpuim |
From Proposition to Program - Embedding the Refinement Calculus in Coq. |
FLOPS |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Jay A. McCarthy, Burke Fetscher, Max S. New, Daniel Feltey, Robert Bruce Findler |
A Coq Library for Internal Verification of Running-Times. |
FLOPS |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Arthur Blot, Pierre-Évariste Dagand, Julia Lawall |
From Sets to Bits in Coq. |
FLOPS |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Alexander John Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink |
Coqoon - An IDE for Interactive Proof Development in Coq. |
TACAS |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Greg Morrisett |
Challenges in compiling Coq. |
PPDP |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Xiyue Zhang, Weijiang Hong, Yi Li 0010, Meng Sun 0002 |
Reasoning About Connectors in Coq. |
FACS |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Christian Doczkal, Gert Smolka |
Two-Way Automata in Coq. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Paul Brunet, Damien Pous, Insa Stucke |
Cardinalities of Finite Relations in Coq. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Paolo Torrini |
Modular Dependent Induction in Coq, Mendler-Style. |
ITP |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Hiroaki Date, Noriaki Yoshiura |
Computational Verification of Network Programs for Several OpenFlow Switches in Coq. |
ICCSA (2) |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Sebastian Böhne, Maria Knobelsdorf, Christoph Kreitz |
Mathematisches Argumentieren und Beweisen mit dem Theorembeweiser Coq. |
HDI |
2016 |
DBLP BibTeX RDF |
|
16 | Tahina Ramananandro, Paul Mountcastle, Benoît Meister, Richard Lethin |
A unified Coq framework for verifying C programs with floating-point computations. |
CPP |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Amin Timany, Bart Jacobs 0002 |
Category Theory in Coq 8.5. |
FSCD |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Sorin Stratulat |
Structural vs. Cyclic Induction: A Report on Some Experiments with Coq. |
SYNASC |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Ke Zhang, Zongyan Qiu |
Coq Implementation of OO Verification Framework VeriJ. |
SEFM |
2016 |
DBLP DOI BibTeX RDF |
|
16 | Nelma Moreira, David Pereira, Simão Melo de Sousa |
Deciding Kleene algebra terms equivalence in Coq. |
J. Log. Algebraic Methods Program. |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Nicolas Magaud, Agathe Chollet, Laurent Fuchs |
Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective. |
Ann. Math. Artif. Intell. |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Qian Wang, Xiaoyu Song, William N. N. Hung, Ming Gu 0001, Jiaguang Sun 0001 |
Scalable Verification of a Generic End-Around-Carry Adder for Floating-Point Units by Coq. |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Éric Tanter, Nicolas Tabareau |
Gradual Certified Programming in Coq. |
CoRR |
2015 |
DBLP BibTeX RDF |
|
16 | Théo Zimmermann, Hugo Herbelin |
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant. |
CoRR |
2015 |
DBLP BibTeX RDF |
|
16 | Ali Assaf 0002, Raphaël Cauderlier |
Mixing HOL and Coq in Dedukti (Extended Abstract). |
PxTP@CADE |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Amin Timany, Bart Jacobs 0002 |
Category Theory in Coq 8.5. |
CoRR |
2015 |
DBLP BibTeX RDF |
|
16 | Jaap Boender, Florian Kammüller, Rajagopal Nagarajan |
Formalization of Quantum Protocols using Coq. |
QPL |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Bruno Barras, Carst Tankink, Enrico Tassi |
Asynchronous processing of Coq documents: from the kernel up to the user interface. |
CoRR |
2015 |
DBLP BibTeX RDF |
|
16 | Floris van Doorn |
Propositional Calculus in Coq. |
CoRR |
2015 |
DBLP BibTeX RDF |
|
16 | Sylvie Boldo, Catherine Lelay, Guillaume Melquiond |
Coquelicot: A User-Friendly Library of Real Analysis for Coq. |
Math. Comput. Sci. |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Yi Li 0010, Meng Sun 0002 |
Modeling and verification of component connectors in Coq. |
Sci. Comput. Program. |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis |
Mtac: A monad for typed tactic programming in Coq. |
J. Funct. Program. |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Éric Tanter, Nicolas Tabareau |
Gradual certified programming in Coq. |
DLS |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Delphine Demange, David Pichardie, Léo Stefanesco |
Verifying Fast and Sparse SSA-Based Optimizations in Coq. |
CC |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Beta Ziliani, Matthieu Sozeau |
A unification algorithm for Coq featuring universe polymorphism and overloading. |
ICFP |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Christoph Benzmüller, Bruno Woltzenlogel Paleo |
Interacting with Modal Logics in the Coq Proof Assistant. |
CSR |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Stergios Chatzikyriakidis |
Natural Language Reasoning using Coq: Interaction and Automation. |
TALN |
2015 |
DBLP BibTeX RDF |
|
16 | Mohammad-Mahdi Bidmeshki, Yiorgos Makris |
VeriCoq: A Verilog-to-Coq converter for proof-carrying hardware automation. |
ISCAS |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Fuli Zhou, Xu Wang, Chen Shan, Ni Lin |
COQ math model case study for self-brand automobile industry. |
IEEM |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Filip Sieczkowski, Ales Bizjak, Lars Birkedal |
ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Petar Maksimovic, Alan Schmitt |
HOCore in Coq. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Bruno Barras, Carst Tankink, Enrico Tassi |
Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface. |
ITP |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Steven Schäfer, Gert Smolka, Tobias Tebbi |
Completeness and Decidability of de Bruijn Substitution Algebra in Coq. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Jingyuan Cao, Ming Fu, Xinyu Feng 0001 |
Practical Tactics for Verifying C Programs in Coq. |
CPP |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Richard Dapoigny, Patrick Barlatier |
A Coq-Based Axiomatization of Tarski's Mereogeometry. |
COSIT |
2015 |
DBLP DOI BibTeX RDF |
|
16 | Théo Zimmermann, Hugo Herbelin |
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant. |
CICM (Work in Progress) |
2015 |
DBLP BibTeX RDF |
|
16 | Beta Ziliani |
Interactive typed tactic programming in the Coq proof assistant. |
|
2015 |
RDF |
|
16 | Nuno Gaspar, Ludovic Henrio, Eric Madelaine |
Bringing Coq into the World of GCM Distributed Applications. |
Int. J. Parallel Program. |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Pierre Castéran, Jacques Garrigue, David Nowak |
Summer School on Coq (NII Shonan Meeting 2014-9). |
NII Shonan Meet. Rep. |
2014 |
DBLP BibTeX RDF |
|
16 | Hai Wan, Anping He, Zhiyang You, Xibin Zhao |
Formal Proof of a Machine Closed Theorem in Coq. |
J. Appl. Math. |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Qian Wang, Xiaoyu Song, Ming Gu 0001, Jia-Guang Sun 0001 |
Functional Verification of High Performance Adders in COQ. |
J. Appl. Math. |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Jason Gross, Adam Chlipala, David I. Spivak |
Experience Implementing a Performant Category-Theory Library in Coq. |
CoRR |
2014 |
DBLP BibTeX RDF |
|
16 | Carst Tankink |
PIDE for Asynchronous Interaction with Coq. |
UITP |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Parvez Mahmood Khan, M. M. Sufyan Beg |
Measuring Cost of Quality (CoQ) on SDLC Projects is Indispensible for Effective Software Quality Assurance. |
CoRR |
2014 |
DBLP BibTeX RDF |
|
16 | Jónathan Heras, Ekaterina Komendantskaya |
Proof Pattern Search in Coq/SSReflect. |
CoRR |
2014 |
DBLP BibTeX RDF |
|
16 | Cezary Kaliszyk, Lionel Mamane, Josef Urban |
Machine Learning of Coq Proof Guidance: First Experiments. |
CoRR |
2014 |
DBLP BibTeX RDF |
|
16 | Jónathan Heras, Ekaterina Komendantskaya |
HoTT formalisation in Coq: Dependency Graphs \& ML4PG. |
CoRR |
2014 |
DBLP BibTeX RDF |
|
16 | Christopher Meiklejohn |
Vector Clocks in Coq: An Experience Report. |
CoRR |
2014 |
DBLP BibTeX RDF |
|
16 | Jónathan Heras, Ekaterina Komendantskaya |
Recycling Proof Patterns in Coq: Case Studies. |
Math. Comput. Sci. |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Stergios Chatzikyriakidis, Zhaohui Luo |
Natural Language Inference in Coq. |
J. Log. Lang. Inf. |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Braibant, Jacques-Henri Jourdan, David Monniaux |
Implementing and Reasoning About Hash-consed Data Structures in Coq. |
J. Autom. Reason. |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Julianna Zsido |
Theorem of Three Circles in Coq. |
J. Autom. Reason. |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Richard Dapoigny, Patrick Barlatier |
Formalizing Context for Domain Ontologies in Coq. |
Context in Computing |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Robbert Krebbers |
Separation Algebras for C Verification in Coq. |
VSTTE |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Jean-François Dufourd |
Pointer Program Derivation Using Coq: Graphs and Schorr-Waite Algorithm. |
ICFEM |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Beta Ziliani, Matthieu Sozeau |
Towards a better-behaved unification algorithm for Coq. |
UNIF |
2014 |
DBLP BibTeX RDF |
|
16 | Gérard P. Huet, Hugo Herbelin |
30 years of research and development around Coq. |
POPL |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Cezary Kaliszyk, Lionel Mamane, Josef Urban |
Machine Learning of Coq Proof Guidance: First Experiments. |
SCSS |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Véronique Benzaken, Evelyne Contejean, Stefania Dumbrava |
A Coq Formalization of the Relational Data Model. |
ESOP |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Chao Li, Liang Dou, Zongyuan Yang |
A metamodeling level transformation from UML sequence diagrams to Coq. |
ICTCS |
2014 |
DBLP BibTeX RDF |
|
16 | Richard Dapoigny, Patrick Barlatier |
Specifying Well-Formed Part-Whole Relations in Coq. |
ICCS |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Yoichi Hirai, Reynald Affeldt |
What could Coq do for Database Software? - A Progress Report. |
JFLA |
2014 |
DBLP BibTeX RDF |
|
16 | Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous |
Formal verification in Coq of program properties involving the global state effect. |
JFLA |
2014 |
DBLP BibTeX RDF |
|
16 | Matthieu Sozeau, Nicolas Tabareau |
Universe Polymorphism in Coq. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Evmorfia-Iro Bartzia, Pierre-Yves Strub |
A Formal Library for Elliptic Curves in the Coq Proof Assistant. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Jason Gross, Adam Chlipala, David I. Spivak |
Experience Implementing a Performant Category-Theory Library in Coq. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Kento Emoto, Frédéric Loulergue, Julien Tesson |
A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Robert Dockins |
Formalized, Effective Domain Theory in Coq. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Cyril Cohen, Anders Mörtberg |
A Coq Formalization of Finitely Presented Modules. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Christian Doczkal, Gert Smolka |
Completeness and Decidability Results for CTL in Coq. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Simon Robillard |
Catamorphism Generation and Fusion Using Coq. |
SYNASC |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Alberto Ciaffaglione, Ivan Scagnetto |
Internal Adequacy of Bookkeeping in Coq. |
LFMTP |
2014 |
DBLP DOI BibTeX RDF |
|
16 | Washington de Carvalho Segundo, Flávio L. C. de Moura, Daniel Ventura |
Formalizing a Named Explicit Substitutions Calculus in Coq. |
CICM Workshops |
2014 |
DBLP BibTeX RDF |
|
16 | Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles |
Computing persistent homology within Coq/SSReflect. |
ACM Trans. Comput. Log. |
2013 |
DBLP DOI BibTeX RDF |
|
16 | Julianna Zsido |
Theorem of three circles in Coq. |
CoRR |
2013 |
DBLP BibTeX RDF |
|