| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Abhishek Anand, Vincent Rahli |
Towards a Formally Verified Proof Assistant.  |
ITP  |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Robbert Krebbers, Xavier Leroy, Freek Wiedijk |
Formal C Semantics: CompCert and the C Standard. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Gerwin Klein, Ruben Gamboa (eds.) |
Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-François Dufourd |
Hypermap Specification and Certified Linked Implementation Using Orbits. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Sandrine Blazy, Vincent Laporte, David Pichardie |
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Cyril Cohen, Anders Mörtberg |
A Coq Formalization of Finitely Presented Modules. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Nao Hirokawa, Aart Middeldorp, Christian Sternagel |
A New and Formalized Proof of Abstract Completion. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Rob Arthan |
HOL Constant Definition Done Right. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Magnus O. Myreen, Jared Davis |
The Reflective Milawa Theorem Prover Is Sound - (Down to the Machine Code That Runs It). |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin Ring, Christoph Lüth |
Collaborative Interactive Theorem Proving with Clide. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Gregory Malecha, Adam Chlipala, Thomas Braibant |
Compositional Computational Reflection. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Matichuk, Makarius Wenzel, Toby C. Murray |
An Isabelle Proof Method Language. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens |
HOL with Definitions: Semantics, Soundness, and a Verified Implementation. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Tobias Nipkow, Dmitriy Traytel |
Unified Decision Procedures for Regular Expression Equivalence. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Vincent Aravantinos, Sofiène Tahar |
Implicational Rewriting Tactics in HOL. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Timothy Bourke, Rob J. van Glabbeek, Peter Höfner |
Showing Invariance Compositionally for a Process Algebra for Network Protocols. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Makarius Wenzel |
Asynchronous User Interaction and Tool Integration in Isabelle/PIDE. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Guyslain Naves, Arnaud Spiwack |
Balancing Lists: A Proof Pearl. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Umair Siddique, Mohamed Yousri Mahmoud, Sofiène Tahar |
On the Formalization of Z-Transform in HOL. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Jared Davis, Anna Slobodová, Sol Swords |
Microcode Verification - Another Piece of the Microprocessor Verification Puzzle. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Doczkal, Gert Smolka |
Completeness and Decidability Results for CTL in Coq. |
ITP |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Cyril Cohen |
Pragmatic Quotient Types in Coq. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Magnus O. Myreen, Scott Owens, Ramana Kumar |
Steps towards Verified Implementations of HOL Light. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux 0001, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry |
A Machine-Checked Proof of the Odd Order Theorem. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Panagiotis Manolios |
Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk, Alexander Krauss 0001 |
Scalable LCF-Style Proof Translation. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Jian Xu, Xingyuan Zhang, Christian Urban |
Mechanising Turing Machines and Computability Theory in Isabelle/HOL. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Jörg Endrullis, Dimitri Hendriks, Martin Bodin |
Circular Coinduction in Coq Using Bisimulation-Up-To Techniques. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Kaustuv Chaudhuri |
Subformula Linking as an Interaction Method. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Assia Mahboubi, Enrico Tassi |
Canonical Structures for the Working Coq User. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Braibant, Jacques-Henri Jourdan, David Monniaux |
Implementing Hash-Consed Structures in Coq. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Carsten Schürmann |
Certifying Voting Protocols. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Evgeny Makarov, Bas Spitters |
The Picard Algorithm for Ordinary Differential Equations in Coq. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Evan Austin, Perry Alexander |
Stateless Higher-Order Logic with Quantified Types. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Lammich |
Automatic Data Refinement. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Guillaume Claret, Lourdes Del Carmen González-Huesca, Yann Régis-Gianas, Beta Ziliani |
Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Etienne Mabille, Marc Boyer, Loïc Fejoz, Stephan Merz |
Towards Certifying Network Calculus. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Makarius Wenzel |
Shared-Memory Multiprocessing for Interactive Theorem Proving. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Damien Pous |
Kleene Algebra with Tests and Coq Tools for while Programs. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Emmanuel Polonowski |
Automatically Generated Infrastructure for De Bruijn Syntaxes. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-François Monin, Xiaomu Shi |
Handcrafted Inversions Made Operational on Operational Semantics. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr. |
Mechanical Verification of SAT Refutations with Extended Resolution. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Sandrine Blazy, Christine Paulin-Mohring, David Pichardie (eds.) |
Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | David A. Cock |
Practical Probability: Applying pGCL to Lattice Scheduling. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Pierre Neron |
Square Root and Division Elimination in PVS. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | David L. Rager, Warren A. Hunt Jr., Matt Kaufmann |
A Parallelized Theorem Prover for a Logic with Parallel Execution. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Haftmann, Alexander Krauss 0001, Ondrej Kuncar, Tobias Nipkow |
Data Refinement in Isabelle/HOL. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Viktor Vafeiadis |
Adjustable References. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Kenji Miyamoto, Fredrik Nordvall Forsberg, Helmut Schwichtenberg |
Program Extraction from Nested Definitions. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Lochbihler |
Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Norrish, Brian Huffman |
Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Dominique Bolignano |
Applying Formal Methods in the Large. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers |
Communicating Formal Proofs: The Case of Flyspeck. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | René Thiemann |
Formalizing Bounded Increase. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Vincent Rahli, Mark Bickford, Abhishek Anand |
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Alasdair Armstrong, Georg Struth, Tjark Weber |
Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban |
MaSh: Machine Learning for Sledgehammer. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Liya Liu, Osman Hasan, Vincent Aravantinos, Sofiène Tahar |
Formal Reasoning about Classified Markov Chains in HOL. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | K. Rustan M. Leino |
Automating Theorem Proving with SMT. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Johannes Hölzl, Fabian Immler, Brian Huffman |
Type Classes and Filters for Mathematical Analysis in Isabelle/HOL. |
ITP |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Asperti |
A Compact Proof of Decidability for Regular Expression Equivalence. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Reynald Affeldt, Manabu Hagiwara |
Formalization of Shannon's Theorems in SSReflect-Coq. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Magnus O. Myreen |
Functional Programs: Conversions between Deep and Shallow Embeddings. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | William Mansky, Elsa L. Gunter |
Using Locales to Define a Rely-Guarantee Temporal Logic. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | David Greenaway, June Andronick, Gerwin Klein |
Bridging the Gap: Automatic Verified Abstraction of C. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew Gacek |
Abella: A Tutorial. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Anthony C. J. Fox |
Directions in ISA Specification. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Ramana Kumar, Joe Hurd |
Standalone Tactics Using OpenTheory. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Xingyuan Zhang, Christian Urban, Chunhan Wu |
Priority Inheritance Protocol Proved Correct. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Georges Gonthier, Enrico Tassi |
A Language of Patterns for Subterm Selection. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Dimitrios Vytiniotis, Thierry Coquand, David Wahlstedt |
Stop When You Are Almost-Full - Adventures in Constructive Termination. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Tobias Nipkow |
Abstract Interpretation of Annotated Commands. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Gerwin Klein, Rafal Kolanski, Andrew Boyton |
Mechanised Separation Algebra. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson |
MetiTarski: Past and Future. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin |
Computer-Aided Cryptographic Proofs. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Lammich, Thomas Tuerk |
Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Nils Anders Danielsson |
Bag Equivalence via a Proof-Relevant Membership Relation. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Ruben Gamboa, John R. Cowles |
A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin-Mohring |
Towards Provably Robust Watermarking. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Cyril Cohen |
Construction of Real Algebraic Numbers in Coq. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Lennart Beringer, Amy P. Felty (eds.) |
Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Sternagel, René Thiemann |
Certification of Nontermination Proofs. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Patrick Michel, Arnd Poetzsch-Heffter |
Verifying and Generating WP Transformers for Procedures on Complex Data. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Jesper Bengtson, Jonas Braband Jensen, Lars Birkedal |
Charge! - A Framework for Higher-Order Separation Logic in Coq. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | André Platzer |
A Differential Operator Approach to Equational Differential Invariants - (Invited Paper). |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Christian Blanchette, Andrei Popescu 0001, Daniel Wand, Christoph Weidenbach |
More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Marino Miculan, Marco Paviotti |
Synthesis of Distributed Mobile Programs Using Monadic Types in Coq. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Maxime Dénès, Anders Mörtberg, Vincent Siles |
A Refinement-Based Approach to Computational Algebra in Coq. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabian Immler, Johannes Hölzl |
Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Noschinski |
Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem. |
ITP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Don S. Batory |
Towards Verification of Product Lines. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Lochbihler, Lukas Bulwahn |
Animating the Formalised Semantics of a Java-Like Language. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk (eds.) |
Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Scott Owens, Peter Böhm, Francesco Zappa Nardelli, Peter Sewell |
Lem: A Lightweight Tool for Heavyweight Semantics. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Georges Gonthier |
Point-Free, Set-Free Concrete Linear Algebra. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Magnus O. Myreen, Jared Davis |
A Verified Runtime for a Verified Theorem Prover. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal |
Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Norrish |
Mechanised Computability Theory. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Bart Jacobs 0001, Ronny Wichers Schreur |
Logical Formalisation and Analysis of the Mifare Classic Card in PVS. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Chunhan Wu, Xingyuan Zhang, Christian Urban |
A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license