| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | John Harrison 0001 |
Without Loss of Generality.  |
TPHOLs  |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Adam Naumowicz, Artur Kornilowicz |
A Brief Overview of Mizar. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau |
Packaging Mathematical Structures. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
Formalization of Algebra, Coercive subtyping, SSReflect, Type inference, Coq |
| 1 | Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies |
VCC: A Practical System for Verifying Concurrent C. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Scott Owens, Susmit Sarkar, Peter Sewell |
A Better x86 Memory Model: x86-TSO. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Nick Benton, Andrew Kennedy, Carsten Varming |
Some Domain Theory and Denotational Semantics in Coq. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter V. Homeier |
The HOL-Omega Logic. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Tuerk |
A Formalisation of Smallfoot in HOL. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Javier de Dios, Ricardo Peña-Marí |
Formal Certification of a Resource-Aware Language Implementation. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
memory management, functional languages, compiler verification |
| 1 | Carsten Schürmann 0001 |
The Twelf Proof Assistant. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Keiko Nakata 0001, Tarmo Uustalu |
Trace-Based Coinductive Operational Semantics for While. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Bove, Peter Dybjer, Ulf Norell |
A Brief Overview of Agda - A Functional Language with Dependent Types. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Lochbihler |
Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Berghofer, Markus Reiter |
Formalizing the Logic-Automaton Connection. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Jesper Bengtson, Joachim Parrow |
Psi-calculi in Isabelle. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | David A. Basin, Srdjan Capkun, Patrick Schaller, Benedikt Schmidt 0002 |
Let's Get Physical: Models and Methods for Real-World Security Protocols. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | John Harrison 0001 |
HOL Light: An Overview. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel (eds.) |
Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Jinshuang Wang, Huabing Yang, Xingyuan Zhang |
Liveness Reasoning with Isabelle/HOL. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
Liveness Proof, Inductive Protocol Verification, Parametric Fairness, Probabilistic Model |
| 1 | Alexander Schimpf, Stephan Merz, Jan-Georg Smaus |
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Chad E. Brown, Gert Smolka |
Extended First-Order Logic. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Jeremy E. Dawson, Alwen Tiu |
Formalising Observer Theory for Environment-Sensitive Bisimulation. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Osman Hasan, Sanaz Khan Afshar, Sofiène Tahar |
Formal Analysis of Optical Waveguides in HOL. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Wouter Swierstra |
A Hoare Logic for the State Monad. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Berghofer, Lukas Bulwahn, Florian Haftmann |
Turning Inductive into Equational Specifications. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Magnus O. Myreen, Michael J. C. Gordon |
Verified LISP Implementations on ARM, x86 and PowerPC. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Frédéric Dabrowski, David Pichardie |
A Certified Data Race Analysis for a Java-like Language. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Stéphane Le Roux 0001 |
Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
sequential game theory, effective generalisation, abstraction, induction, Coq |
| 1 | Nicolas Julien, Ioana Pasca |
Formal Verification of Exact Computations Using Newton's Method. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Rafal Kolanski, Gerwin Klein |
Types, Maps and Separation Logic. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi |
Hints in Unification. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David A. Cock, Michael Norrish |
Mind the Gap. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Brian Huffman |
A Purely Definitional Universal Domain. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | René Thiemann, Christian Sternagel |
Certification of Termination Proofs Using CeTA. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew McCreight |
Practical Tactics for Separation Logic. |
TPHOLs |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Berghofer, Christian Urban |
Nominal Inversion Principles. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Pierre Courtieu, Julien Forest, Xavier Urbain |
Certifying a Termination Criterion Based on Graphs, without Graphs. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, J Strother Moore |
An ACL2 Tutorial. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca |
Canonical Big Operators. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow |
The Isabelle Framework. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | David A. Cock, Gerwin Klein, Thomas Sewell |
Secure Microkernels, State Monads and Scalable Refinement. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Yves Bertot |
A Short Presentation of Coq. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Lukas Bulwahn, Alexander Krauss 0001, Florian Haftmann, Levent Erkök, John Matthews |
Imperative Functional Programming with Isabelle/HOL. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Sam Owre, Natarajan Shankar |
A Brief Overview of PVS. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Sayan Mitra, K. Mani Chandy |
A Formalized Theory for Verifying Stability and Convergence of Automata in PVS. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Jens Brandt 0001, Klaus Schneider 0001 |
Formal Reasoning About Causality Analysis. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | David R. Lester |
Real Number Calculations and Theorem Proving. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
Computable Reals, Exact Arithmetic, Theorem Proving, PVS, Higher-order Logic |
| 1 | Matthieu Sozeau, Nicolas Oury |
First-Class Type Classes. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Hasan Amjad |
LCF-Style Propositional Simplification with BDDs and SAT Solvers. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Laurent Théry |
Proof Pearl: Revisiting the Mini-rubik in Coq. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Polyvios Pratikakis, Jeffrey S. Foster, Michael Hicks 0001, Iulian Neamtiu |
Formalizing Soundness of Contextual Effects. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Wasserrab, Andreas Lochbihler |
Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Otmane Aït Mohamed, César A. Muñoz, Sofiène Tahar (eds.) |
Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Klaus Aehlig, Florian Haftmann, Tobias Nipkow |
A Compiled Implementation of Normalization by Evaluation. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Steven P. Miller |
Will This Be Formal? |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
model checking, Formal methods, theorem proving, avionics |
| 1 | Holger Gast |
Lightweight Separation. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Russell O'Connor |
Certified Exact Transcendental Real Number Computation in Coq. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Mike Gordon |
Twenty Years of Theorem Proving for HOLs Past, Present and Future. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Sascha Böhme, K. Rustan M. Leino, Burkhart Wolff |
HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Bove, Venanzio Capretta |
A Type of Partial Recursive Functions. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Konrad Slind, Michael Norrish |
A Brief Overview of HOL4. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Lukas Bulwahn, Alexander Krauss 0001, Tobias Nipkow |
Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Constance L. Heitmeyer |
On the Utility of Formal Methods in the Development and Certification of Software. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Zhaozhong Ni, Dachuan Yu, Zhong Shao |
Using XCAP to Certify Realistic Systems Code: Machine Context Management. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | François Garillot, Benjamin Werner |
Simple Types in Type Theory: Deep and Shallow Encodings. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka |
Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Laurent Théry, Guillaume Hanrot |
Primality Proving with Elliptic Curves. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | John Harrison 0001 |
Verifying Nonlinear Real Formulas Via Sums of Squares. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Osman Hasan, Sofiène Tahar |
Verification of Expectation Properties for Discrete Random Variables in HOL. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | David Delahaye, Catherine Dubois, Jean-Frédéric Étienne |
Extracting Purely Functional Contents from Logical Inductive Types. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Liggesmeyer |
Formal Techniques in Software Engineering: Correct Software and Safe Systems. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Klaus Schneider 0001, Jens Brandt 0001 (eds.) |
Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Tom Ridge |
Operational Reasoning for Concurrent Caml Programs and Weak Memory Models. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Makarius Wenzel, Burkhart Wolff |
Building Formal Method Tools in the Isabelle/Isar Framework. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Steven Obua |
Proof Pearl: Looping Around the Orbit. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Eunsuk Kang, Mark D. Aagaard |
Improving the Usability of HOL Through Controlled Automation Tactics. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry |
A Modular Formalisation of Finite Group Theory. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Sprenger 0001, David A. Basin |
A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | James Reynolds |
Automatically Translating Type and Function Definitions from HOL to ACL2. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Freek Wiedijk |
Mizar's Soft Type System. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Jeremy E. Dawson |
Formalising Generalised Substitutions. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
general correctness, generalised substitution |
| 1 | David Aspinall 0001, Jaroslav Sevcík |
Formalising Java's Data Race Free Guarantee. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Sandrine Blazy |
Separation Logic for Small-Step cminor. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | José-Antonio Alonso, Joaquín Borrego-Díaz, María-José Hidalgo, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina |
A Formally Verified Prover for the ALC Description Logic. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Yasuhiko Minamide |
Verified Decision Procedures on Context-Free Grammars. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Norbert Völker |
HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Joe Hurd |
Proof Pearl: The Termination Analysis of Terminator. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Norrish, René Vestergaard |
Proof Pearl: De Bruijn Terms Really Do Work. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, Konrad Slind |
Proof Pearl: Wellfounded Induction on the Ordinals Up to epsilon 0. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Lawrence C. Paulson, Kong Woei Susanto |
Source-Level Proof Reconstruction for Interactive Theorem Proving. |
TPHOLs |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Tobias Nipkow, Lawrence C. Paulson |
Proof Pearl: Defining Functions over Finite Sets. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew M. Pitts |
Alpha-Structural Recursion and Induction. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Claude Marché, Christine Paulin-Mohring |
Reasoning About Java Programs with Aliasing and Frame Conditions. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Joe Hurd, Thomas F. Melham (eds.) |
Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic |
Mechanized Metatheory for the Masses: The PoplMark Challenge. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Tuerk, Klaus Schneider 0001 |
From PSL to LTL: A Formal Validation in HOL. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | David A. Naumann |
Verifying a Secure Information Flow Analyzer. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Brian Huffman, John Matthews, Peter White |
Axiomatic Constructor Classes in Isabelle/HOLCF. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith |
Meta Reasoning in ACL2. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Benjamin Grégoire, Assia Mahboubi |
Proving Equalities in a Commutative Ring Done Right in Coq. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license