default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID6th HUG 1993: Vancouver, BC, Canada
- Jeffrey J. Joyce, Carl-Johan H. Seger:
Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG '93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings. Lecture Notes in Computer Science 780, Springer 1994, ISBN 3-540-57826-9 - Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson:
Program Verification using HOL-UNITY. 1-15 - Kim Dam Petersen:
Graph model of LAMBDA in Higher Order Logic. 16-28 - Cui Zhang, Robert J. Shaw, Ronald A. Olsson, Karl N. Levitt, Myla Archer, Mark R. Heckman, Gregory D. Benson:
Mechanizing a Programming Logic for the Concurrent Programming Language microSR in HOL. 29-42 - Don Syme:
Reasoning with the Formal Definition of Standard ML in HOL. 43-60 - Myra Van Inwegen, Elsa L. Gunter:
HOL-ML. 61-74 - Kees G. W. Goossens:
Stucture and Behaviour in Hardware Verification. 75-88 - Catia M. Angelo, Luc J. M. Claesen, Hugo De Man:
Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL. 89-100 - Dirk Eisenbiegler, Klaus Schneider
, Ramayya Kumar:
A Functional Approach for Formalizing Regular Hardware Structures. 101-114 - Laurent Théry:
A Proof Development System for HOL. 115-128 - Rachel E. O. Roxas:
A HOL Package for Reasoning about Relations Defined by Mutual Induction. 129-140 - Elsa L. Gunter:
A Broader Class of Trees for Recursive Type Definitions for HOL. 141-154 - David Lorge Parnas:
Some Theorems We Should Prove. 155-162 - John M. Rushby, Mandayam K. Srivas:
Using PVS to Prove Some Theorems Of David Parnas. 163-173 - John Harrison, Laurent Théry:
Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals. 174-184 - Jeffrey J. Joyce, Carl-Johan H. Seger:
The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover. 185-198 - Juin-Yeu Lu, Shiu-Kai Chin:
Linking HOL to a VLSI CAD System. 199-212 - Klaus Schneider, Ramayya Kumar, Thomas Kropf:
Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic. 213-226 - Anthony McIsaac:
A Formalization of Abstraction in LAMBDA. 227-238 - Tej Arora, Tony Leung, Karl N. Levitt, E. Thomas Schubert, Phillip J. Windley:
Report on the UCD Microcoded Viper Verification Project. 239-252 - Zheng Zhu, Jeffrey J. Joyce, Carl-Johan H. Seger:
Verification of the Tamarack-3 Microprocessor in a Hybrid Verification Environment. 253-266 - David A. Fura, Phillip J. Windley, Arun K. Somani:
Abstraction Techniques for Modeling Real-World Interface Chips. 267-280 - Sofiène Tahar, Ramayya Kumar:
Implementing a Methodology for Formally Verifying RISC Processors in HOL. 281-294 - Sten Agerholm:
Domain Theory in HOL. 295-309 - Ching-Tsun Chou:
Predicates, Temporal Logic, and Simulations. 310-323 - I. S. W. B. Prasetya:
Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties. 324-337 - Nancy A. Day, Jeffrey J. Joyce:
The Semantics of Statecharts in HOL. 338-351 - Monica Nesi:
Value-Passing CCS in HOL. 352-365 - Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi:
TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory. 366-370 - Wai Wong:
Modelling Bit Vectors in HOL: the word library. 371-384 - Klaus Schneider, Ramayya Kumar, Thomas Kropf:
Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification. 385-398 - Mark D. Aagaard, Miriam Leeser, Phillip J. Windley:
Toward a Super Duper Hardware Tactic. 399-412 - Andrew D. Gordon:
A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion. 413-425 - John Harrison:
A HOL Decision Procedure for Elementary Real Algebra. 426-435 - Konrad Slind:
AC Unification in HOL90. 436-449 - Stephen H. Brackin, Shiu-Kai Chin:
Server-Process Restrictiveness in HOL. 450-463 - Matthew J. Morley:
Safety in Railway Signalling Data: A Behavioural Analysis. 464-474 - I. S. W. B. Prasetya:
On the Style of Mechanical Proving. 475-488 - Sreeranga P. Rajan, Jeffrey J. Joyce, Carl-Johan H. Seger:
From Abstract Data Types to Shift Registers: A Case Study in Formal Specification and Verification at Differing Levels of Abstraction using Theorem Proving and Symbolic Simulation. 489-500 - Victor Carreño:
Verification in Higher Order Logic of Mutual Exclusion Algorithm. 501-513 - Sara Kalvala:
Using Isabelle to Prove Simple Theorems. 514-517
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-01-29 21:25 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
