Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
16 | Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters |
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSF ![In: 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021, pp. 1-15, 2021, IEEE, 978-1-7281-7607-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Peter Schwabe, Benoît Viguier, Timmy Weerwag, Freek Wiedijk |
A Coq proof of the correctness of X25519 in TweetNaCl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSF ![In: 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021, pp. 1-16, 2021, IEEE, 978-1-7281-7607-9. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Xiaokun Luan, Meng Sun 0002 |
Modeling and Verification of CKB Consensus Protocol in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
QRS Companion ![In: 21st IEEE International Conference on Software Quality, Reliability and Security, QRS 2021 - Companion, Hainan, China, December 6-10, 2021, pp. 660-667, 2021, IEEE, 978-1-6654-7836-6. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Dominique Larchey-Wendling |
Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSCD ![In: 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference)., pp. 18:1-18:20, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-191-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Conor Reynolds |
Formalizing the Institution for Event-B in the Coq Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ABZ ![In: Rigorous State-Based Methods - 8th International Conference, ABZ 2021, Ulm, Germany, June 9-11, 2021, Proceedings, pp. 162-166, 2021, Springer, 978-3-030-77542-1. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Rajeev Goré, Revantha Ramanayake, Ian Shillito |
Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TABLEAUX ![In: Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings, pp. 299-313, 2021, Springer, 978-3-030-86058-5. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Lennard Gäher, Fabian Kunze |
Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 20:1-20:18, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Dominik Kirst, Marc Hermes |
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 23:1-23:20, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti |
Formalising a Turing-Complete Choreographic Language in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 15:1-15:18, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Pierre Nigron, Pierre-Évariste Dagand |
Reaching for the Star: Tale of a Monad in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)., pp. 29:1-29:19, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-188-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Véronique Benzaken, Sarah Cohen-Boulakia, Evelyne Contejean, Chantal Keller, Rébecca Zucchini |
A Coq formalization of data provenance. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pp. 152-162, 2021, ACM, 978-1-4503-8299-1. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Dominik Kirst, Felix Rech |
The generalised continuum hypothesis implies the axiom of choice in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pp. 313-326, 2021, ACM, 978-1-4503-8299-1. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Koundinya Vajjha, Avraham Shinnar, Barry M. Trager, Vasily Pestun, Nathan Fulton |
CertRL: formalizing convergence proofs for value and policy iteration in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pp. 18-31, 2021, ACM, 978-1-4503-8299-1. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters |
Extracting smart contracts tested and verified in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pp. 105-121, 2021, ACM, 978-1-4503-8299-1. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Pierre-Léo Bégay, Pierre Crégut, Jean-François Monin |
Developing and certifying Datalog optimizations in coq/mathcomp. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pp. 163-177, 2021, ACM, 978-1-4503-8299-1. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Lucien Rakotomalala, Pierre Roux, Marc Boyer |
Verifying Min-Plus Computations with Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
NFM ![In: NASA Formal Methods - 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021, Proceedings, pp. 287-303, 2021, Springer, 978-3-030-76383-1. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Pengyu Nie 0001, Karl Palmskog, Junyi Jessy Li, Milos Gligoric 0001 |
Roosterize: Suggesting Lemma Names for Coq Verification Projects Using Deep Learning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICSE (Companion Volume) ![In: 43rd IEEE/ACM International Conference on Software Engineering: Companion Proceedings, ICSE Companion 2021, Madrid, Spain, May 25-28, 2021, pp. 21-24, 2021, IEEE, 978-1-6654-1219-3. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Yannick Forster 0002 |
Church's Thesis and Related Axioms in Coq's Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference)., pp. 21:1-21:19, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-175-7. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban |
Online Machine Learning Techniques for Coq: A Comparison. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM ![In: Intelligent Computer Mathematics - 14th International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings, pp. 67-83, 2021, Springer, 978-3-030-81096-2. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
16 | Fritjof Bornebusch |
Coq meets CλaSH: proposing a hardware design synthesis flow that combines proof assistants with functional hardware description languages ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2021 |
RDF |
|
16 | Ángel Francisco Zúñiga Chávez |
Semántica natural como marco de verificación de compiladores en Coq ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2021 |
RDF |
|
16 | Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic |
Interaction trees: representing recursive and impure programs in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proc. ACM Program. Lang. ![In: Proc. ACM Program. Lang. 4(POPL), pp. 51:1-51:32, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Zheng Cheng, Massimo Tisi, Rémi Douence |
CoqTL: a Coq DSL for rule-based model transformation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Softw. Syst. Model. ![In: Softw. Syst. Model. 19(2), pp. 425-439, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Zheng Yang 0007, Hang Lei, Weizhong Qian |
A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-Based Service Smart Contracts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Access ![In: IEEE Access 8, pp. 21411-21436, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Tianyu Sun, Wensheng Yu |
A Formal System of Axiomatic Set Theory in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Access ![In: IEEE Access 8, pp. 21510-21523, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters |
Extracting Smart Contracts Tested and Verified in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2012.09138, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Dominique Larchey-Wendling, Yannick Forster 0002 |
Hilbert's Tenth Problem in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2003.04604, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Yannick Forster 0002 |
Church's thesis and related axioms in Coq's type theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2009.00416, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Koundinya Vajjha, Avraham Shinnar, Vasily Pestun, Barry M. Trager, Nathan Fulton |
CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2009.11403, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Lasse Blaauwbroek, Josef Urban, Herman Geuvers |
Tactic Learning and Proving for the Coq Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2003.09140, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Wenjun Shi, Qinxiang Cao, Yuxin Deng, Hanru Jiang, Yuan Feng 0001 |
Symbolic Reasoning about Quantum Circuits in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2005.11023, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Lasse Blaauwbroek, Josef Urban, Herman Geuvers |
The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2008.00120, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Boro Sitnikovski |
Formalizing line editors in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2006.03525, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Dominik Kirst, Dominique Larchey-Wendling |
Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2004.07390, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Boro Sitnikovski, Biljana Stojcevska, Lidija Goracinova-Ilieva, Irena Stojmenovska |
PubSub implementation in Haskell with formal verification in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2005.09452, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Pengyu Nie 0001, Karl Palmskog, Junyi Jessy Li, Milos Gligoric 0001 |
Learning to Format Coq Code Using Language Models. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2006.16743, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Dimitur Nikolaev Krustev |
Experience Report: Smuggling a Little Bit of Coq Inside a CAD Development Context (Extended Abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2007.00695, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Pengyu Nie 0001, Karl Palmskog, Junyi Jessy Li, Milos Gligoric 0001 |
Deep Generation of Coq Lemma Names Using Elaborated Terms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2004.07761, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Burak Ekici, Cezary Kaliszyk |
Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Math. Comput. Sci. ![In: Math. Comput. Sci. 14(3), pp. 533-549, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Christian Doczkal, Damien Pous |
Graph Theory in Coq: Minors, Treewidth, and Isomorphisms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 64(5), pp. 795-825, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Jiawei Wang, Ming Fu, Lei Qiao, Xinyu Feng 0001 |
Formalizing SPARCv8 instruction set architecture in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Sci. Comput. Program. ![In: Sci. Comput. Program. 187, pp. 102371, 2020. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Lasse Blaauwbroek, Josef Urban, Herman Geuvers |
Tactic Learning and Proving for the Coq Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020., pp. 138-150, 2020, EasyChair. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Hao Bu, Meng Sun 0002 |
Towards Modeling and Verification of the CKB Block Synchronization Protocol in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFEM ![In: Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1-3, 2021, Proceedings, pp. 287-296, 2020, Springer, 978-3-030-63405-6. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Elaine Li, Traian Serbanuta, Denisa Diaconescu, Vlad Zamfir, Grigore Rosu |
Formalizing Correct-by-Construction Casper in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE ICBC ![In: IEEE International Conference on Blockchain and Cryptocurrency, ICBC 2020, Toronto, ON, Canada, May 2-6, 2020, pp. 1-3, 2020, IEEE, 978-1-7281-6680-3. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Bruno Bernardo, Raphaël Cauderlier, Guillaume Claret, Arvid Jakobsson, Basile Pesin, Julien Tesson |
Making Tezos Smart Contracts More Reliable with Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISoLA (3) ![In: Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III, pp. 60-72, 2020, Springer, 978-3-030-61466-9. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Matteo Cavada, Andrea Colò, Alberto Momigliano |
MutantChick: Type-Preserving Mutation Analysis for Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CILC ![In: Proceedings of the 35th Italian Conference on Computational Logic - CILC 2020, Rende, Italy, October 13-15, 2020., pp. 105-112, 2020, CEUR-WS.org. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP BibTeX RDF |
|
16 | Rafael Castro G. Silva, Cristiano D. Vasconcellos, Karina Girardi Roggia |
Monadic W in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SBLP ![In: SBLP '20: 24th Brazilian Symposium on Programming Languages, Natal, Rio Grande do Norte, Brazil, October 19-23, 2020, pp. 25-32, 2020, ACM, 978-1-4503-8943-3. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi |
Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description). ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSCD ![In: 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference)., pp. 34:1-34:21, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-155-9. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Zheng Yang 0007, Hang Lei, Weizhong Qian, Zehui Yan, Weiru Zeng |
A Resolution for Scalability Problem of Record Datatype Based Formal Memory Models in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSAE ![In: CSAE 2020: The 4th International Conference on Computer Science and Application Engineering, Sanya, China, October 20-22, 2020, pp. 54:1-54:8, 2020, ACM, 978-1-4503-7772-0. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Matteo Manighetti, Dale Miller 0001, Alberto Momigliano |
Two Applications of Logic Programming to Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy., pp. 10:1-10:19, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-182-5. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Dominik Kirst, Dominique Larchey-Wendling |
Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR (2) ![In: Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, pp. 79-96, 2020, Springer, 978-3-030-51053-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Pengyu Nie 0001, Karl Palmskog, Junyi Jessy Li, Milos Gligoric 0001 |
Deep Generation of Coq Lemma Names Using Elaborated Terms. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR (2) ![In: Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, pp. 97-118, 2020, Springer, 978-3-030-51053-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Lukasz Czajka 0001 |
Practical Proof Search for Coq by Type Inhabitation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR (2) ![In: Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, pp. 28-57, 2020, Springer, 978-3-030-51053-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Thayonara Alves, Leopoldo Teixeira, Vander Alves, Thiago M. Castro |
Porting the Software Product Line Refinement Theory to the Coq Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SBMF ![In: Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, Proceedings, pp. 192-209, 2020, Springer, 978-3-030-63881-8. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters |
ConCert: a smart contract certification framework in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020., pp. 215-228, 2020, ACM, 978-1-4503-7097-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Simon Spies, Yannick Forster 0002 |
Undecidability of higher-order unification formalised in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020., pp. 143-157, 2020, ACM, 978-1-4503-7097-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Yannick Forster 0002, Kathrin Stark |
Coq à la carte: a practical approach to modular syntax with binders. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020., pp. 186-200, 2020, ACM, 978-1-4503-7097-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Talia Ringer, Alex Sanchez-Stern, Dan Grossman, Sorin Lerner |
REPLica: REPL instrumentation for Coq analysis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020., pp. 99-113, 2020, ACM, 978-1-4503-7097-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Yannick Forster 0002, Fabian Kunze, Maxi Wuttke |
Verified programming of Turing machines in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020., pp. 114-128, 2020, ACM, 978-1-4503-7097-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Christian Doczkal, Damien Pous |
Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020., pp. 325-337, 2020, ACM, 978-1-4503-7097-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Letan, Yann Régis-Gianas |
FreeSpec: specifying, verifying, and executing impure computations in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020., pp. 32-46, 2020, ACM, 978-1-4503-7097-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Kush Jain, Karl Palmskog, Ahmet Çelik, Emilio Jesús Gallego Arias, Milos Gligoric 0001 |
mCoq: mutation analysis for Coq verification projects. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICSE (Companion Volume) ![In: ICSE '20: 42nd International Conference on Software Engineering, Companion Volume, Seoul, South Korea, 27 June - 19 July, 2020, pp. 89-92, 2020, ACM, 978-1-4503-7122-3. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Samir Ouchani, Khaled Khebbeb, Meriem Hafsi |
Towards Enhancing Security and Resilience in CPS: A Coq-Maude based Approach. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AICCSA ![In: 17th IEEE/ACS International Conference on Computer Systems and Applications, AICCSA 2020, Antalya, Turkey, November 2-5, 2020, pp. 1-6, 2020, IEEE, 978-1-7281-8577-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Lasse Blaauwbroek, Josef Urban, Herman Geuvers |
The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM ![In: Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, pp. 271-277, 2020, Springer, 978-3-030-53517-9. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Kathrin Stark |
Mechanising syntax with binders in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2020 |
RDF |
|
16 | Matthieu Sozeau, Cyprien Mangin |
Equations reloaded: high-level dependently-typed functional programming and proving in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proc. ACM Program. Lang. ![In: Proc. ACM Program. Lang. 3(ICFP), pp. 86:1-86:29, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Zheng Yang 0007, Hang Lei |
FEther: An Extensible Definitional Interpreter for Smart-Contract Verifications in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Access ![In: IEEE Access 7, pp. 37770-37791, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, Ivan Scagnetto |
LF+ in Coq for "fast and loose" reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Formaliz. Reason. ![In: J. Formaliz. Reason. 12(1), pp. 11-51, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Jakob Botsch Nielsen, Bas Spitters |
Smart Contract Interactions in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1911.04732, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon M. Moore, Karl Palmskog, Lucas Peña, Grigore Rosu |
Towards a Verified Model of the Algorand Consensus Protocol in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1907.05523, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic |
Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1906.00046, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Florian Steinberg 0001, Laurent Théry, Holger Thies |
Quantitative continuity and computable analysis in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1904.13203, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Zheng Yang 0007, Hang Lei, Weizong Qian |
A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1902.08726, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Gérard Berry, Lionel Rieg |
Towards Coq-verified Esterel Semantics and Compiling. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1909.12582, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Jonathan Chan, William J. Bowman |
Practical Sized Typing for Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1912.05601, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Yannick Forster 0002, Fabian Kunze |
A certifying extraction with time bounds from Coq to call-by-value $λ$-calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1904.11818, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Danil Annenkov, Bas Spitters |
Towards a Smart Contract Verification Framework in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1907.10674, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Gustavo Carvalho, Igor Meira |
Modelling and testing timed data-flow reactive systems in Coq from controlled natural-language requirements. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1910.13553, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli |
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
PxTP ![In: Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019., pp. 18-26, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Andrei Arusoaie |
A Formal Semantics of Findel in Coq (Short Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1909.05464, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, Julien Tesson |
Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1909.08671, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa |
A Definitional Implementation of the Lax Logical Framework LLFP in Coq, for Supporting Fast and Loose Reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP@LICS ![In: Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@LICS 2019, Vancouver, Canada, 22nd June 2019., pp. 8-23, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Pierre Boutry, Charly Gries, Julien Narboux, Pascal Schreck |
Parallel Postulates and Continuity Axioms: A Mechanized Study in Intuitionistic Logic Using Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 62(1), pp. 1-68, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Yannick Forster 0002, Gert Smolka |
Call-by-Value Lambda Calculus as a Model of Computation in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 63(2), pp. 393-413, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Xiyue Zhang, Weijiang Hong, Yi Li 0010, Meng Sun 0002 |
Reasoning about connectors using Coq and Z3. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Sci. Comput. Program. ![In: Sci. Comput. Program. 170, pp. 27-44, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Zhenwei Ma, Gang Chen |
基于Coq记录的矩阵形式化方法 (Matrix Formalization Based on Coq Record). ![Search on Bibsonomy](Pics/bibsonomy.png) |
计算机科学 ![In: 计算机科学 46(7), pp. 139-145, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Sergey Bozhko, Leyla Khatbullina, Semyon V. Grigorev |
Bar-Hillel Theorem Mechanization in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
WoLLIC ![In: Logic, Language, Information, and Computation - 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, July 2-5, 2019, Proceedings, pp. 264-281, 2019, Springer, 978-3-662-59532-9. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Nitin Bhatia, Meenakshi D'Souza, Sujit Kumar Chakrabarti |
Formalizing GPU Instruction Set Architecture in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISEC ![In: Proceedings of the 12th Innovations on Software Engineering Conference (formerly known as India Software Engineering Conference), ISEC 2019, Pune, India, February 14-16, 2019, pp. 28:1-28:5, 2019, ACM, 978-1-4503-6215-3. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Salwa Souaf, Frédéric Loulergue |
A First Step in the Translation of Alloy to Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFEM ![In: Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings, pp. 455-469, 2019, Springer, 978-3-030-32408-7. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Jolan Philippe, Frédéric Loulergue |
Parallel programming with Coq: map and reduce skeletons on trees. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAC ![In: Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing, SAC 2019, Limassol, Cyprus, April 8-12, 2019, pp. 1578-1581, 2019, ACM, 978-1-4503-5933-7. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Benjamin Ferrell, Jun Duan, Kevin W. Hamlen |
CUDA au Coq: A Framework for Machine-validating GPU Assembly Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DATE ![In: Design, Automation & Test in Europe Conference & Exhibition, DATE 2019, Florence, Italy, March 25-29, 2019, pp. 474-479, 2019, IEEE, 978-3-9819263-2-3. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, Julien Tesson |
Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FM Workshops (1) ![In: Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I, pp. 368-379, 2019, Springer, 978-3-030-54993-0. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Jakob Botsch Nielsen, Bas Spitters |
Smart Contract Interactions in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FM Workshops (1) ![In: Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I, pp. 380-391, 2019, Springer, 978-3-030-54993-0. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon M. Moore, Karl Palmskog, Lucas Peña, Grigore Rosu |
Towards a Verified Model of the Algorand Consensus Protocol in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FM Workshops (1) ![In: Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I, pp. 362-367, 2019, Springer, 978-3-030-54993-0. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Siran Lei, Mengqi Cheng, Jianguo Jiang |
Tactics for Proving Separation Logic Assertion in Coq Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICVISP ![In: ICVISP 2019: 3rd International Conference on Vision, Image and Signal Processing, Vancouver, BC, Canada, August 26-28, 2019, pp. 99:1-99:5, 2019, ACM, 978-1-4503-7625-9. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Yuxin Deng, Jean-François Monin |
Formalisation of Probabilistic Testing Semantics in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
The Art of Modelling Computational Systems ![In: The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy - Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, pp. 276-292, 2019, Springer, 978-3-030-31174-2. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Kosuke Murata, Kento Emoto |
Recursion Schemes in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APLAS ![In: Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, pp. 202-221, 2019, Springer, 978-3-030-34174-9. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Alexander Bagnall, Gordon Stewart 0001 |
Certifying the True Error: Machine Learning in Coq with Verified Generalization Guarantees. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AAAI ![In: The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2019, Honolulu, Hawaii, USA, January 27 - February 1, 2019., pp. 2662-2669, 2019, AAAI Press, 978-1-57735-809-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Florian Faissole, George A. Constantinides, David B. Thomas |
Formalizing Loop-Carried Dependencies in Coq for High-Level Synthesis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FCCM ![In: 27th IEEE Annual International Symposium on Field-Programmable Custom Computing Machines, FCCM 2019, San Diego, CA, USA, April 28 - May 1, 2019, pp. 315, 2019, IEEE, 978-1-7281-1131-5. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Raul Fervari, Francisco Trucco, Beta Ziliani |
Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DaLí ![In: Dynamic Logic. New Trends and Applications - Second International Workshop, DaLí 2019, Porto, Portugal, October 7-11, 2019, Proceedings, pp. 3-18, 2019, Springer, 978-3-030-38807-2. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|