Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Marco Benini, Sara Kalvala, Dirk Nowotka |
Program Abstraction in a Higher-Order Logic Framework. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Anna Mikhajlova, Joakim von Wright |
Proving Isomorphism of First-Order Logic Proof Systems in HOL. |
TPHOLs |
1998 |
DBLP DOI BibTeX RDF |
|
1 | Albert John Camilleri |
A Hybrid Approach to Verifying Liveness in a Symmetric Multi-Processor. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Bruno Dutertre, Steve A. Schneider |
Using a PVS Embedding of CSP to Verify Authentication Protocols. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Santen |
A Theory of Structured Model-Based Specifications in Isabelle/HOL. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Sten Agerholm, Jacob Frost |
An Isabelle-Based Theorem Prover for VDM-SL. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Doron A. Peled |
Verification for Robust Specification. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Daniel Hirschkoff |
A Full Formalisation of pi-Calculus Theory in the Calculus of Constructions. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | James H. Andrews |
Executing Formal Specifications by Translation to Higher Order Logic Programming. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Oscar Slotosch |
Higher Order Quotients and their Implementation in Isabelle HOL. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Konrad Slind |
Derivation and Use of Induction Schemes in Higher-Order Logic. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Myla Archer, Constance L. Heitmeyer |
Human-Style Theorem Proving Using PVS. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Martin Simons 0001 |
Proof Presentation for Isabelle. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Boutheina Chetali, Barbara Heyd |
Formal Verification of Concurrent Programs in LP and in COQ: A Comparative Analysis. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
theorem prover methodology, Larch Prover, Computer Checked Proof, Formal Verification, Unity, Coq |
1 | Vincent Zammit |
A Comparative Study of Coq and HOL. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Elsa L. Gunter, Amy P. Felty (eds.) |
Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | John Harrison 0001 |
Verifying the Accuracy of Polynomial Approximations in HOL. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Deepak Kapur |
Rewriting, Decision Procedures and Lemma Speculation for Automated Hardware Verification. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Långbacka, Joakim von Wright |
Refining Reactive Systems in HOL Using Action Systems. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Robert L. Constable |
ML Programming in Constructive Type Theory (abstract). |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Markus Wenzel 0001 |
Type Classes and Overloading in Higher-Order Logic. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Dowek |
Proof Normalization for a First-Order Formulation of Higher-Order Logic. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Marco Devillers, W. O. David Griffioen, Olaf Müller |
Possibly Infinite Sequences in Theorem Provers: A Comparative Study. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Wolfgang Naraschewski |
Towards an Object-Oriented Progification Language. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Takahisa Mohri |
On Formalization of Bicategory Theory. |
TPHOLs |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Cornelia Pusch |
Verification of Compiler Correctness for the WAM. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Paul E. Black, Phillip J. Windley |
Inference Rules for Programming Languages with Side Effects in Expressions. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Barbara Heyd, Pierre Crégut |
A Modular Coding of UNITY in COQ. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Bruno Dutertre |
Elements of Mathematical Analysis in PVS. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Linas Laibinis |
Using Lattice Theory in Higher Order Logic. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Michael J. Butler, Thomas Långbacka |
Program Derivation Using the Refinement Calculator. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | David A. Basin, Stefan Friedrich 0001 |
Modeling a Hardware Synthesis Methodology in Isabelle. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Sten Agerholm |
Translating Specifications in VDM-SL to PVS. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Vincent Zammit |
A Mechanisation of Computability Theory in HOL. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | John Harrison 0001 |
Stålmarck's Algorithm as a HOL Derived Rule. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Dirk Eisenbiegler, Christian Blumenröhr, Ramayya Kumar |
Implementation Issues About the Embedding of Existing High Level Synthesis Algorithms in HOL. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Bernhard Reus |
Synthetic Domain Theory in Type Theory: Another Logic of Computable Functions. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Stephen H. Brackin |
Deciding Cryptographic Protocol Adequacy with HOL: The Implementation. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Solange Coupet-Grimal, Line Jakubiec |
Coq and Hardware Verification: A Case Study. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Holger Busch |
Proving Liveness of Fair Transition Systems. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Mark R. Heckman, Cui Zhang, Brian R. Becker, Dave Peticolas, Karl N. Levitt, Ronald A. Olsson |
Towards Applying the Composition Principle to Verify a Microkernel Operating System. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Alan Smaill, Ian Green |
Higher-Order Annotated Terms for Proof Search. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | John Harrison 0001 |
A Mizar Mode for HOL. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Sofiène Tahar, Paul Curzon |
A Comparison of MDG and HOL for Hardware Verification. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Dieter Nazareth, Tobias Nipkow |
Formal Verification of Algorithm W: The Monomorphic Case. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Joakim von Wright, Jim Grundy, John Harrison 0001 (eds.) |
Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Michael J. C. Gordon |
Set Theory, Higher Order Logic or Both? |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Konrad Slind |
Function Definition in Higher-Order Logic. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Sten Agerholm, Ilya Beylin, Peter Dybjer |
A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Graham Collins |
A Proof Tool for Reasoning About Functional Programs. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Andrew D. Gordon 0001, Thomas F. Melham |
Five Axioms of Alpha-Conversion. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Mats Larsson |
Improving the Result of High-Level Synthesis Using Interactive Transformational Design. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Douglas J. Howe |
Importing Mathematics from HOL into Nuprl. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Kolyang 0001, Thomas Santen, Burkhart Wolff |
A Structure Preserving Encoding of Z in Isabelle/HOL. |
TPHOLs |
1996 |
DBLP DOI BibTeX RDF |
|
1 | Graham Collins, Don Syme |
A Theory of Finite Maps. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Elsa L. Gunter, Leonid Libkin |
Interfacing HOL90 with a Functional Database Query Language. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Ralf Reetz |
Deep Embedding VHDL. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Don Syme |
A New Interface for HOL - Ideas, Issues and Implementation. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Långbacka, Rimvydas Ruksenas, Joakim von Wright |
TkWinHOL: A Tool for Window Inference in HOL. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | E. Thomas Schubert, Phillip J. Windley, Jim Alves-Foss (eds.) |
Higher Order Logic Theorem Proving and Its Applications, 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995, Proceedings |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Otmane Aït Mohamed |
Mechanizing a pi-Calculus Equivalence in HOL. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Jean-Paul Bodeveix, Mamoun Filali |
On the Refinement of symmetric memory protocols. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Wai Wong |
Recording and Checking HOL Proofs. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Paul E. Black, Phillip J. Windley |
Autotically Synthesized Term Denotation Predicates: A Proof Aid. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Sten Agerholm, Michael J. C. Gordon |
Experiments with ZF Set Theory in HOL and Isabelle. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Cui Zhang, Brian R. Becker, Mark R. Heckman, Karl N. Levitt, Ronald A. Olsson |
A Hierarchical Method for Reasoning about Distributed Programming Languages. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Morten Welinder |
Very Efficient Conversions. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | John Harrison 0001 |
Floating Point Verification in HOL. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | E. Thomas Schubert, Sarah Mocas |
A Mechanized Logic for Secure Key Escrow Protocol Verification. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Mitsuharu Yamamoto, Shin-ya Nishizaki, Masami Hagiya, Yozo Toda |
Formalization of Planar Graphs. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Paul Loewenstein |
Formal Verification of Counterflow Pipeline Architecture. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Stephen H. Brackin |
Deciding Cryptographic Protocol Adequacy with HOL. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Sten Agerholm |
Non-primitive Recursive Function Definitions. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Richard J. Boulton |
Combining Decision Procedures in the HOL System. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Paul Curzon |
Virtual Theories. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Franz Regensburger |
HOLCF: Higher Order Logic of Computable Functions. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Jang Dae Kim, Shiu-Kai Chin |
Formal Verification of Serial Pipeline Multipliers. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | John Harrison 0001 |
Inductive Definitions: Automation and Application. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Dirk Eisenbiegler, Ramayya Kumar |
An Automata Theory Dedicated towards Formal Circuit Synthesis. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Holger Busch |
A Practical Method for Reasoning about Distributed Systems in a Theorem Prover. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Sara Kalvala |
A Formulation of TLA in Isabelle. |
TPHOLs |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Ching-Tsun Chou |
A Formal Theory of Undirected Graphs in Higher-Order Logic. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Catia M. Angelo, Luc J. M. Claesen, Hugo De Man |
Reasoning About a Class of Linear Systems of Equations in HOL. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson |
A Graphical Tool for Proving Unity Progress. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Forster |
Weak Systems of Set Theory Related to HOL. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Jeffrey J. Joyce, Nancy A. Day, Michael R. Donat |
S: A Machine Readable Specification Notation based on Higher Order Logic. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Stephen H. Brackin |
Providing Tractable Security Analysis in HOL. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | David A. Fura, Arun K. Somani |
Interval-Semantic Component Models and the Efficient Verification of Transaction-Level Circiut Behavior. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Juin-Yeu Lu, Shiu-Kai Chin |
Generating Designs Using an Algorithmic Register Transfer Language with Formal Semantics. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Paul Curzon |
Tracking Design Changes with Formal Verification. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Joakim von Wright |
Representing Higher-Order Logic Proofs in HOL. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Keith Hanna |
Reasoning about Real Circuits. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Holger Busch |
First-Order Automation for Higher-Order-Logic Theorem Proving. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Sofiène Tahar, Ramayya Kumar |
Implementational Issues for Verifying RISC-Pipeline Conflicts in HOL. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Savi Maharaj, Elsa L. Gunter |
Studying the ML Module System in Hol. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | N. G. de Bruijn |
Highlighting the Lambda-free Fragment of Automath. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Mats Larsson |
An Engineering Approach to Formal Digital System Design. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Jean-Paul Bodeveix, Mamoun Filali, P. Roche |
Towards a HOL Theory and Memory. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Nick Chapman, Simon Finn, Michael P. Fourman |
Datatypes in L2. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|
1 | Juanito Camilleri, Vincent Zammit |
Symbolic Animation as a Proof Tool. |
TPHOLs |
1994 |
DBLP DOI BibTeX RDF |
|