| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Laureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio 0001, José-Luis Ruiz-Reina |
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials.  |
ITP  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Reid, Ruben Gamboa |
Automatic Differentiation in ACL2. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Gammie |
Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest, Marc Cavazza |
Structural Analysis of Narratives with the Coq Proof Assistant. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Johannes Hölzl, Armin Heller |
Three Chapters of Measure Theory in Isabelle/HOL. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Tarek Mhamdi, Osman Hasan, Sofiène Tahar |
Formalization of Entropy Measures in HOL. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Ramana Kumar, Tjark Weber |
Validating QBF Validity in HOL4. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Sylvain Heraud, David Nowak |
A Formalization of Polytime Functions. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Matej Urbas, Mateja Jamnik |
Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Phil Scott, Jacques D. Fleuriot |
Composable Discovery Engines for Interactive Theorem Proving. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Ondrej Kuncar |
Proving Valid Quantified Boolean Formulas in HOL Light. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexander Krauss 0001, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl |
Termination of Isabelle Functions via Termination of Rewriting. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Lennart Beringer |
Relational Decomposition. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Anthony C. J. Fox |
LCF-Style Bit-Blasting in HOL4. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein |
seL4 Enforces Integrity. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Kishinevsky, Alexander Gotmanov, Yuriy Viktorov |
Challenges in Verifying Communication Fabrics. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | David Monniaux, Pierre Corbineau |
On the Generation of Positivstellensatz Witnesses in Degenerate Cases. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Georges Gonthier |
Advances in the Formalization of the Odd Order Theorem. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Tobias Nipkow |
Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Renaud Clavel, Laurence Pierre, Régis Leveugle |
Towards Robustness Analysis Using PVS. |
ITP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Christian Blanchette, Tobias Nipkow |
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Panagiotis Manolios, Daron Vroon 0001 |
Interactive Termination Proofs Using Termination Cores. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Anthony C. J. Fox, Magnus O. Myreen |
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | David Cachera, David Pichardie |
A Certified Denotational Abstract Interpreter. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Chantal Keller, Benjamin Werner |
Importing HOL Light into Coq. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Gerwin Klein |
A Formally Verified OS Kernel. Now What? |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Freek Verbeek, Julien Schmaltz |
A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Sol Swords, Warren A. Hunt Jr. |
A Mechanically Verified AIG-to-BDD Conversion Algorithm. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Magnus O. Myreen |
Separation Logic Adapted for Proofs by Rewriting. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthieu Sozeau |
Equations: A Dependent Pattern-Matching Compiler. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Benjamin C. Pierce |
Proof Assistants as Teaching Assistants: A View from the Trenches. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Sascha Böhme, Tjark Weber |
Fast LCF-Style Proof Reconstruction for Z3. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Joe Hendrix, Deepak Kapur, José Meseguer 0001 |
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Ernie Cohen, Bert Schirmer |
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Bas Spitters, Eelis van der Weegen |
Developing the Algebraic Hierarchy with Type Classes in Coq. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Serge Autexier, Dominik Dietrich |
A Tactic Language for Declarative Proofs. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen |
Automated Machine-Checked Hybrid System Safety Proofs. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Amy P. Felty, Brigitte Pientka |
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexander Krauss 0001, Andreas Schropp |
A Mechanized Translation from Higher-Order Logic to Set Theory. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Moa Johansson, Lucas Dixon, Alan Bundy |
Case-Analysis for Rippling and Inductive Proof. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | William Mansky, Elsa L. Gunter |
A Framework for Formal Verification of Compiler Optimizations. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz |
Inductive Consequences in the Calculus of Constructions. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis |
Formal Proof of a Wave Equation Resolution Scheme: The Method Error. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-François Dufourd, Yves Bertot |
Formal Study of Plane Delaunay Triangulation. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Tjark Weber |
Validating QBF Invalidity in HOL4. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Brian Huffman, Christian Urban |
A New Foundation for Nominal Isabelle. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Tarek Mhamdi, Osman Hasan, Sofiène Tahar |
On the Formalization of the Lebesgue Integration Theory in HOL. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry |
Extending Coq with Imperative Features and Its Application to SAT Verification. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Ramana Kumar, Michael Norrish |
(Nominal) Unification by Recursive Descent with Triangular Substitutions. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin |
Programming Language Techniques for Cryptographic Proofs. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Braibant, Damien Pous |
An Efficient Coq Tactic for Deciding Kleene Algebras. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Arthur Charguéraud |
The Optimal Fixed Point Combinator. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Lammich, Andreas Lochbihler |
The Isabelle Collections Framework. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | John R. Cowles, Ruben Gamboa |
Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, Lawrence C. Paulson (eds.) |
Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Douglas J. Howe |
Higher-Order Abstract Syntax in Isabelle/HOL. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license