Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
16 | Grygoriy Zholtkevych |
Event Universes: Specification and Analysis Using Coq Proof Assistant. |
ICTERI Workshops |
2019 |
DBLP BibTeX RDF |
|
16 | Pascal Fradet, Xiaojie Guo 0003, Jean-François Monin, Sophie Quinton |
CertiCAN: A Tool for the Coq Certification of CAN Analysis Results. |
RTAS |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Guillaume Bertholon, Érik Martin-Dorel, Pierre Roux |
Primitive Floats in Coq. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Talia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman |
Ornaments for Proof Reuse in Coq. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Florian Steinberg 0001, Laurent Théry, Holger Thies |
Quantitative Continuity and Computable Analysis in Coq. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry |
Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Lukasz Czajka 0001 |
First-Order Guarded Coinduction in Coq. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Yannick Forster 0002, Fabian Kunze |
A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. |
ITP |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Yannick Forster 0002, Steven Schäfer, Simon Spies, Kathrin Stark |
Call-by-push-value in coq: operational, equational, and denotational theory. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Yannick Forster 0002, Dominik Kirst, Gert Smolka |
On synthetic undecidability in coq, with an application to the entscheidungsproblem. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Véronique Benzaken, Evelyne Contejean |
A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra. |
CPP |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Dominique Larchey-Wendling, Yannick Forster 0002 |
Hilbert's Tenth Problem in Coq. |
FSCD |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Ahmet Çelik, Karl Palmskog, Marinela Parovic, Emilio Jesús Gallego Arias, Milos Gligoric 0001 |
Mutation Analysis for Coq. |
ASE |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Jan Christiansen, Sandra Dylus, Niels Bunkenburg |
Verifying effectful Haskell programs in Coq. |
Haskell@ICFP |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Xiyue Zhang, Yi Li 0010, Weijiang Hong, Meng Sun 0002 |
Using Recurrent Neural Network to Predict Tactics for Proving Component Connector Properties in Coq. |
TASE |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Claudio Sacerdoti Coen |
A Plugin to Export Coq Libraries to XML. |
CICM |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Dennis Müller 0001, Florian Rabe 0001, Claudio Sacerdoti Coen |
The Coq Library as a Theory Graph. |
CICM |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Joachim Breitner, Antal Spector-Zabusky, Yao Li 0004, Christine Rizkallah, John Wiegley, Stephanie Weirich |
Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report). |
Proc. ACM Program. Lang. |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer |
Mtac2: typed tactics for backward reasoning in Coq. |
Proc. ACM Program. Lang. |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Akira Tanaka, Reynald Affeldt, Jacques Garrigue |
Safe Low-level Code Generation in Coq Using Monomorphization and Monadification. |
J. Inf. Process. |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Alexander John Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink |
Coqoon - An IDE for interactive proof development in Coq. |
Int. J. Softw. Tools Technol. Transf. |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Joachim Breitner, Antal Spector-Zabusky, Yao Li 0004, Christine Rizkallah, John Wiegley, Stephanie Weirich |
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
16 | Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry |
Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
16 | Yves Bertot |
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
16 | Moez A. AbdelGawad |
Finitary-based Domain Theory in Coq: An Early Report. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
16 | Zheng Yang 0007, Hang Lei |
FEther: An Extensible Definitional Interpreter for Smart-contract Verifications in Coq. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
16 | Lukasz Czajka 0001, Burak Ekici, Cezary Kaliszyk |
Concrete Semantics with Coq and CoqHammer. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
16 | Artem Yushkovskiy, Stavros Tripakis |
Comparison of Two Theorem Provers: Isabelle/HOL and Coq. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
16 | Zheng Yang 0007, Hang Lei |
A general formal memory framework in Coq for verifying the properties of programs based on higher-order logic theorem proving with increased automation, consistency, and reusability. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
16 | Lukasz Czajka 0001, Cezary Kaliszyk |
Hammer for Coq: Automation for Dependent Type Theory. |
J. Autom. Reason. |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Christian Doczkal, Gert Smolka |
Regular Language Representations in the Constructive Type Theory of Coq. |
J. Autom. Reason. |
2018 |
DBLP DOI BibTeX RDF |
|
16 | João Alpuim, Wouter Swierstra |
Embedding the refinement calculus in Coq. |
Sci. Comput. Program. |
2018 |
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. |
Sci. Comput. Program. |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Xiyue Zhang, Meng Sun 0002 |
Towards Formal Modeling and Verification of Probabilistic Connectors in Coq (S). |
SEKE |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Yves Bertot |
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq Proofs. |
ICTAC |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Massimo Tisi, Zheng Cheng |
CoqTL: An Internal DSL for Model Transformation in Coq. |
ICMT |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, Guillaume Hiet |
Modular Verification of Programs with Effects and Effect Handlers in Coq. |
FM |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Hideyuki Kawabata, Yuta Tanaka, Mai Kimura, Tetsuo Hironaka |
Traf: A Graphical Proof Tree Viewer Cooperating with Coq Through Proof General. |
APLAS |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Youssef El Bakouny, Dani Mezher |
Scallina: Translating Verified Programs from Coq to Scala. |
APLAS |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Vincent Rahli, Ivana Vukotic, Marcus Völp, Paulo Jorge Esteves Veríssimo |
Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. |
ESOP |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Jérémy Buisson, Seidali Rehab |
Effective Bridging Between Ecore and Coq: Case of a Type-Checker with Proof-Carrying Code. |
MISC |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Catherine Dubois, Sulyvan Weppe |
Towards Coq Formalisation of {log} Set Constraints Resolution. |
SETS@ABZ |
2018 |
DBLP BibTeX RDF |
|
16 | Pascal Fradet, Maxime Lesourd, Jean-François Monin, Sophie Quinton |
A Generic Coq Proof of Typical Worst-Case Analysis. |
RTSS |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Youssef El Bakouny, Dani Mezher |
The Scallina Grammar - Towards a Scala Extraction for Coq. |
SBMF |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau |
Towards Certified Meta-Programming with Typed Template-Coq. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Sylvain Boulmé, Alexandre Maréchal |
A Coq Tactic for Equality Learning in Linear Arithmetic. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Yannick Forster 0002, Edith Heiter, Gert Smolka |
Verification of PCP-Related Computational Reductions in Coq. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Étienne Miquey |
Formalizing Implicative Algebras in Coq. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Véronique Benzaken, Evelyne Contejean, Chantal Keller, Eunice Martins |
A Coq Formalisation of SQL's Execution Engines. |
ITP |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Pawel Wieczorek, Dariusz Biernacki |
A Coq formalization of normalization by evaluation for Martin-Löf type theory. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Damien Rouhling |
A formal proof in Coq of a control function for the inverted pendulum. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman |
Œuf: minimizing the Coq extraction TCB. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Sergueï Lenglet, Alan Schmitt |
HOπ in Coq. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Christian Doczkal, Joachim Bard |
Completeness and decidability of converse PDL in the constructive type theory of Coq. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich |
Total Haskell is reasonable Coq. |
CPP |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Amin Timany, Matthieu Sozeau |
Cumulative Inductive Types In Coq. |
FSCD |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Salwa Souaf, Frédéric Loulergue |
Strong Security Guarantees: From Alloy to Coq (Research Poster). |
HPCS |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, Anthony C. J. Fox |
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4. |
FMCAD |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Ahmet Çelik, Karl Palmskog, Milos Gligoric 0001 |
A regression proof selection tool for coq. |
ICSE (Companion Volume) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | David Braun, Nicolas Magaud, Pascal Schreck |
Formalizing Some "Small" Finite Models of Projective Geometry in Coq. |
AISC |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Diane Gallois-Wong, Sylvie Boldo, Thibault Hilaire |
A Coq Formalization of Digital Filters. |
CICM |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Burak Ekici |
Towards Mac Lane's Comparison Theorem for the (co)Kleisli Construction in Coq. |
CICM Workshops |
2018 |
DBLP BibTeX RDF |
|
16 | Lukasz Czajka 0001, Burak Ekici, Cezary Kaliszyk |
Concrete Semantics with Coq and CoqHammer. |
CICM |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Joshua S. Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar, Jérôme Siméon |
Prototyping a query compiler using Coq (experience report). |
Proc. ACM Program. Lang. |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Tiago Cogumbreiro, Jun Shirako, Vivek Sarkar |
Formalization of Habanero phasers using Coq. |
J. Log. Algebraic Methods Program. |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Bruno Xavier, Carlos Olarte, Giselle Reis, Vivek Nigam |
Mechanizing Focused Linear Logic in Coq. |
LSFA |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Polina Vinogradova, Amy P. Felty, Philip J. Scott |
Formalizing Abstract Computability: Turing Categories in Coq. |
LSFA |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Frédéric Loulergue, Wadoud Bousdira, Julien Tesson |
Calculating Parallel Programs in Coq Using List Homomorphisms. |
Int. J. Parallel Program. |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Alexander Bagnall, Samuel Merten, Gordon Stewart 0001 |
A Library for Algorithmic Game Theory in Ssreflect/Coq. |
J. Formaliz. Reason. |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Sebastian Böhne, Christoph Kreitz |
Learning how to Prove: From the Coq Proof Assistant to Textbook Style. |
ThEdu@CADE |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Youssef El Bakouny, Tristan Crolard, Dani Mezher |
A Coq-based synthesis of Scala programs which are correct-by-construction. |
CoRR |
2017 |
DBLP BibTeX RDF |
|
16 | Yannick Forster 0002, Edith Heiter, Gert Smolka |
Verification of PCP-Related Computational Reductions in Coq. |
CoRR |
2017 |
DBLP BibTeX RDF |
|
16 | Andrew Bedford |
Coqatoo: Generating Natural Language Versions of Coq Proofs. |
CoRR |
2017 |
DBLP BibTeX RDF |
|
16 | Robert Rand 0001, Jennifer Paykin, Steve Zdancewic |
QWIRE Practice: Formal Verification of Quantum Circuits in Coq. |
QPL |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Stéphane Le Roux 0001, Érik Martin-Dorel, Jan-Georg Smaus |
An Existence Theorem of Nash Equilibrium in Coq and Isabelle. |
GandALF |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich |
Total Haskell is Reasonable Coq. |
CoRR |
2017 |
DBLP BibTeX RDF |
|
16 | Sylvie Boldo, Guillaume Melquiond |
Computer Arithmetic and Formal Proofs - Verifying Floating-point Algorithms with the Coq System. |
|
2017 |
RDF |
|
16 | Hernan M. Palombo, Hao Zheng 0001, Jay Ligatti |
POSTER: Towards Precise and Automated Verification of Security Protocols in Coq. |
CCS |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Kenneth Roe, Scott F. Smith 0001 |
Using the coq theorem prover to verify complex data structure invariants. |
MEMOCODE |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds 0001, Clark W. Barrett |
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. |
CAV (2) |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Quentin Carbonneaux, Jan Hoffmann 0002, Thomas W. Reps, Zhong Shao |
Automated Resource Analysis with Coq Proof Objects. |
CAV (2) |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Youssef El Bakouny, Tristan Crolard, Dani Mezher |
A Coq-based synthesis of Scala programs which are correct-by-construction. |
FTfJP@ECOOP |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Jean-Philippe Bernardy, Stergios Chatzikyriakidis |
A Type-Theoretical system for the FraCaS test suite: Grammatical Framework meets Coq. |
IWCS(1) |
2017 |
DBLP BibTeX RDF |
|
16 | Xiaojie Guo 0003, Sophie Quinton, Pascal Fradet, Jean-François Monin |
Work-in-Progress: Toward a Coq-Certified Tool for the Schedulability Analysis of Tasks with Offsets. |
RTSS |
2017 |
DBLP DOI BibTeX RDF |
|
16 | João F. Ferreira 0001, Saul A. Johnson, Alexandra Mendes, Phillip J. Brooke |
Certified Password Quality - A Case Study Using Coq and Linux Pluggable Authentication Modules. |
IFM |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Yannick Forster 0002, Gert Smolka |
Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Dominique Larchey-Wendling |
Typing Total Recursive Functions in Coq. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Cyril Cohen, Damien Rouhling |
A Formal Proof in Coq of LaSalle's Invariance Principle. |
ITP |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Jiawei Wang, Ming Fu, Lei Qiao, Xinyu Feng 0001 |
Formalizing SPARCv8 Instruction Set Architecture in Coq. |
SETTA |
2017 |
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. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Jonas Kaiser, Tobias Tebbi, Gert Smolka |
Equivalence of system f and ź2 in Coq based on context morphism lemmas. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero |
A Coq formal proof of the LaxMilgram theorem. |
CPP |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Jonas Kaiser, Brigitte Pientka, Gert Smolka |
Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga. |
FSCD |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Jolan Philippe, Wadoud Bousdira, Frédéric Loulergue |
Formalization of a Big Graph API in Coq. |
HPCS |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Niki Vazou, Leonidas Lampropoulos, Jeff Polakow |
A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq. |
Haskell |
2017 |
DBLP DOI BibTeX RDF |
|
16 | John Wiegley, Benjamin Delaware |
Using Coq to write fast and correct Haskell. |
Haskell |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Boris Shingarov |
Programming a Smalltalk VM in Coq. |
IWST |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Zhenwei Ma, Gang Chen |
Formal Derivation and Verification of Coordinate Transformations in Theorem Prover Coq. |
DSA |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Yifei Wang, Gang Chen |
Formalization of Laplace Transform in Coq. |
DSA |
2017 |
DBLP DOI BibTeX RDF |
|
16 | Weijiang Hong, M. Saqib Nawaz, Xiyue Zhang, Yi Li 0010, Meng Sun 0002 |
Using Coq for Formal Modeling and Verification of Timed Connectors. |
SEFM Workshops |
2017 |
DBLP DOI BibTeX RDF |
|