default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID9th TPHOLs 1996: Turku, Finland
- Joakim von Wright, Jim Grundy, John Harrison:
Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings. Lecture Notes in Computer Science 1125, Springer 1996, ISBN 3-540-61587-3 - Sten Agerholm:
Translating Specifications in VDM-SL to PVS. 1-16 - Sten Agerholm, Ilya Beylin, Peter Dybjer:
A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. 17-32 - David A. Basin, Stefan Friedrich:
Modeling a Hardware Synthesis Methodology in Isabelle. 33-50 - Paul E. Black, Phillip J. Windley:
Inference Rules for Programming Languages with Side Effects in Expressions. 51-60 - Stephen H. Brackin:
Deciding Cryptographic Protocol Adequacy with HOL: The Implementation. 61-76 - Holger Busch:
Proving Liveness of Fair Transition Systems. 77-92 - Michael J. Butler, Thomas Långbacka:
Program Derivation Using the Refinement Calculator. 93-108 - Graham Collins:
A Proof Tool for Reasoning About Functional Programs. 109-124 - Solange Coupet-Grimal, Line Jakubiec:
Coq and Hardware Verification: A Case Study. 125-139 - Bruno Dutertre:
Elements of Mathematical Analysis in PVS. 141-156 - Dirk Eisenbiegler, Christian Blumenröhr, Ramayya Kumar:
Implementation Issues About the Embedding of Existing High Level Synthesis Algorithms in HOL. 157-172 - Andrew D. Gordon, Thomas F. Melham:
Five Axioms of Alpha-Conversion. 173-190 - Michael J. C. Gordon:
Set Theory, Higher Order Logic or Both? 191-201 - John Harrison:
A Mizar Mode for HOL. 203-220 - John Harrison:
Stålmarck's Algorithm as a HOL Derived Rule. 221-234 - 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. 235-250 - Barbara Heyd, Pierre Crégut:
A Modular Coding of UNITY in COQ. 251-266 - Douglas J. Howe:
Importing Mathematics from HOL into Nuprl. 267-281 - Kolyang, Thomas Santen, Burkhart Wolff:
A Structure Preserving Encoding of Z in Isabelle/HOL. 283-298 - Mats Larsson:
Improving the Result of High-Level Synthesis Using Interactive Transformational Design. 299-314 - Linas Laibinis:
Using Lattice Theory in Higher Order Logic. 315-330 - Dieter Nazareth, Tobias Nipkow:
Formal Verification of Algorithm W: The Monomorphic Case. 331-345 - Cornelia Pusch:
Verification of Compiler Correctness for the WAM. 347-361 - Bernhard Reus:
Synthetic Domain Theory in Type Theory: Another Logic of Computable Functions. 365-380 - Konrad Slind:
Function Definition in Higher-Order Logic. 381-397 - Alan Smaill, Ian Green:
Higher-Order Annotated Terms for Proof Search. 399-413 - Sofiène Tahar, Paul Curzon:
A Comparison of MDG and HOL for Hardware Verification. 415-430 - Vincent Zammit:
A Mechanisation of Computability Theory in HOL. 431-446
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 2026-08-29 00:13 CEST 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, funded, and maintained by:
Schloss Dagstuhl - Leibniz Center for Informatics is a member of the Leibniz Association and is funded by the federal government of Germany and the states of Germany, especially Saarland and Rhineland‑Palatinate.
