Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Pertti Kellomäki |
A Structural Embedding of Ocsid in PVS. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Natarajan Shankar |
Using Decision Procedures with a Higher-Order Logic. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Irene Schena |
HELM and the Semantic Math-Web. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Pavel Naumov, Mark-Oliver Stehr, José Meseguer 0001 |
The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability). |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Giampaolo Bella, Lawrence C. Paulson |
Mechanical Proofs about a Non-repudiation Protocol. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Louise A. Dennis, Alan Smaill |
Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Ana Bove, Venanzio Capretta |
Nested General Recursion and Partiality in Type Theory. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Andrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey, Ursula Martin, Sam Owre |
Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Mario Cáccamo, Glynn Winskel |
A Higher-Order Calculus for Categories. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Gertrud Bauer, Markus Wenzel 0001 |
Calculational Reasoning Revisited (An Isabelle/Isar Experience). |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Bart Jacobs 0001 |
JavaCard Program Verification. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Matt Fairtlough, Michael Mendler, Xiaochun Cheng |
Abstraction and Refinement in Higher Order Logic. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
1 | David Hemer, Ian J. Hayes, Paul A. Strooper |
Refinement Calculus for Logic Programming in Isabelle/HOL. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu 0003 |
Proving Hybrid Protocols Correct. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
1 | R. D. Arthan |
An Irrational Construction of R from Z. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
1 | John Harrison 0001 |
Formal Verification of IA-64 Division Algorithms. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Abdel Mokkedem, Tim Leonard |
Formal Verification of the Alpha 21364 Network Protocol. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | M. Randall Holmes |
A Strong and Mechanizable Grand Logic. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Jim Grundy |
Verified Optimizations for the Intel IA-64 Architecture. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Robert Pollack |
Dependently Typed Records for Representing Mathematical Structure. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Robin Milner |
Graphical Theories of Interactive Systems: Can a Proof Assistant Help? |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Victor Carreño, César A. Muñoz |
Aircraft Trajectory Modeling and Altering Algorithm Verification. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Mickaël Kerboeuf, David Nowak, Jean-Pierre Talpin |
Specification and Verification of a Steam-Boiler with Signal-Coq. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
the steam-boiler problem, theorem proving, synchronous programming |
1 | Linas Laibinis, Joakim von Wright |
Functional Procedures in Higher-Order Logic. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Ewen Denney |
A Prototype Proof Translator from HOL to Coq. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Konrad Slind |
Another Look at Nested Recursion. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Herman Geuvers, Freek Wiedijk, Jan Zwanenburg |
Equational Reasoning via Partial Reflection. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Bruno Barras |
Programming and Computing in HOL. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Antonia Balaa, Yves Bertot |
Fix-Point Equations for Well-Founded Recursion in Type Theory. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Venanzio Capretta |
Recursive Families of Inductive Types. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Bernhard Reus, Tatjana Hein |
Towards a Machine-Checked Java Specification Book. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Jason Hickey, Aleksey Nogin |
Fast Tactic-Based Theorem Proving. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Marieke Huisman, Bart Jacobs 0001 |
Inheritance in Higher Order Logic: Modeling and Reasoning. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Stefan Berghofer, Tobias Nipkow |
Proof Terms for Simply Typed Higher Order Logic. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Mark D. Aagaard, John Harrison 0001 (eds.) |
Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Lüth, Burkhart Wolff |
TAS - A Generic Window Inference System. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Hanne Gottliebsen |
Transcendental Functions and Continuity Checking in PVS. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Roope Kaivola, Mark D. Aagaard |
Divider Circuit Verification with Model Checking and Theorem Proving. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Michael J. C. Gordon |
Reachability Programming in HOL98 Using BDDs. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Catherine Dubois |
Proving ML Type Soundness Within Coq. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic |
Routing Information Protocol in HOL/SPIN. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Larry Wos |
Appendix: Conjectures Concerning Proof, Design, and Verification. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Larry Wos, Branden Fitelson |
Automating the Search for Answers to Open Questions. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Stephan Merz |
Weak Alternating Automata in Isabelle/HOL. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Pierre Letouzey, Laurent Théry |
Formalizing Stålmarck's Algorithm in Coq. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Robert P. Colwell, Bob Brennan |
Intel's Formal Verification Experience on the Willamette Development. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Jacques D. Fleuriot |
On the Mechanization of Real Analysis in Isabelle/HOL. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Martin Hofmann 0001, Francis Tang |
Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Paul B. Jackson |
Total-Correctness Refinement for Sequential Reactive Systems. |
TPHOLs |
2000 |
DBLP DOI BibTeX RDF |
|
1 | Florian Kammüller, Markus Wenzel 0001, Lawrence C. Paulson |
Locales - A Sectioning Concept for Isabelle. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Venanzio Capretta |
Universal Algebra in Type Theory. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Klaus Schneider 0001, Dirk W. Hoffmann |
A HOL Conversion for Translating Linear Time Temporal Logic to omega-Automata. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Mark Staples |
Representing WP Semantics in Isabelle/ZF. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Don Syme |
Three Tactic Theorem Proving. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Stefan Berghofer, Markus Wenzel 0001 |
Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Norbert Völker |
Disjoint Sums over Type Classes in HOL. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Olga Caprotti, Arjeh M. Cohen |
Connecting Proof Checkers and Computer Algebra Using OpenMath. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Nancy A. Day, Jeffrey J. Joyce |
Symbolic Functional Evaluation. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Vincent Zammit |
On the Implementation of an Extensible Declarative Proof Language. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Bernd Grobauer, Olaf Müller |
From I/O Automata to Timed I/O Automata. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Simon Ambler, Roy L. Crole |
Mechanized Operational Semantics via (Co)Induction. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Solange Coupet-Grimal, Line Jakubiec |
Hardware Verification Using Co-induction in COQ. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Markus Wenzel 0001 |
Isar - A Generic Interpretative Approach to Readable Formal Proof Documents. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | John Harrison 0001 |
A Machine-Checked Theory of Floating Point Arithmetic. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Dominique Bolignano |
Formal Methods and Security Evaluation (Invited Talk). |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Kropf |
Recent Advancements in Hardware Verification - How to Make Theorem Proving Fit for an Industrial Usage. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Mark D. Aagaard, Robert B. Jones, Carl-Johan H. Seger |
Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Holger Pfeifer, Harald Rueß |
Polytypic Proof Construction. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | John Matthews |
Recursive Function Definition over Coinductive Types. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Santen |
Isomorphisms - A Link Between the Shallow and the Deep. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Haiyan Xiong, Paul Curzon, Sofiène Tahar |
Importing MDG Verification Results into HOL. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin-Mohring, Laurent Théry (eds.) |
Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Joe Hurd |
Integrating Gandalf and HOL. |
TPHOLs |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Rimvydas Ruksenas, Joakim von Wright |
A Tool for Data Refinement. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | John Harrison 0001 |
Formalizing Basic First Order Model Theory. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | John Harrison 0001 |
Formalizing Dijkstra. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Mitsuharu Yamamoto, Koichi Takahashi, Masami Hagiya, Shin-ya Nishizaki, Tetsuo Tamai |
Formalization of Graph Search Algorithms and Its Applications. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Richard J. Boulton |
Generating Embeddings from Denotational Descriptions. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Jim Grundy, Malcolm C. Newey (eds.) |
Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Wolfgang Naraschewski, Markus Wenzel 0001 |
Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | François Puitg, Jean-François Dufourd |
Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Hajime Sawamura, Daisaku Asanuma |
Mechanizing Relevant Logics with HOL. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Roderick Moten |
Exploiting Parallelism in Interactive Theorem Provers. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | James L. Caldwell |
Classical Propositional Decidability via Nuprl Proof Extraction. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Paul B. Jackson |
Verifying a Garbage Collection Algorithm. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Karthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson 0001, Davor Obradovic, Pamela Zave |
The Village Telephone System: A Case Study in Formal Software Engineering. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Douglas J. Howe |
A Type Annotation Scheme for Nuprl. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | W. O. David Griffioen, Marieke Huisman |
A Comparison of PVS and Isabelle/HOL. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Naren Narasimhan, Ranga Vemuri |
On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Elsa L. Gunter |
Adding External Decision Procedures to HOL90 Securely. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Tobias Nipkow |
Verified Lexical Analysis. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Joakim von Wright |
Extending Window Inference. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Chuck C. Liang |
Free Variables and Subexpressions in Higher-Order Meta Logic. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Friedrich W. von Henke, Stephan Pfab, Holger Pfeifer, Harald Rueß |
Case Studies in Meta-Level Theorem Proving. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Karsten Konrad |
HOT: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Maxim Lifantsev, Leo Bachmair |
An LPO-based Termination Ordering for Higher-Order Terms without lambda-abstraction. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | David Nowak, Jean-René Beauvais, Jean-Pierre Talpin |
Co-inductive Axiomatization of a Synchronous Language. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Richard J. Boulton, Konrad Slind, Alan Bundy, Michael J. C. Gordon |
An Interface between Clam and HOL. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Peter V. Homeier, David F. Martin |
Mechanical Verification of Total Correctness through Diversion Verification Conditions. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Olaf Müller |
I/O Automata and Beyond: Temporal Logic and Abstraction in Isabelle. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|