default search action
11th TPHOLs 1998: Canberra, Australia
- Jim Grundy, Malcolm C. Newey:
Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings. Lecture Notes in Computer Science 1479, Springer 1998, ISBN 3-540-64987-5
Invited Papers
- Tobias Nipkow:
Verified Lexical Analysis. 1-15 - Joakim von Wright:
Extending Window Inference. 17-32
Refereed Papers
- Marco Benini, Sara Kalvala, Dirk Nowotka:
Program Abstraction in a Higher-Order Logic Framework. 33-48 - Karthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Davor Obradovic, Pamela Zave:
The Village Telephone System: A Case Study in Formal Software Engineering. 49-66 - Richard J. Boulton:
Generating Embeddings from Denotational Descriptions. 67-86 - Richard J. Boulton, Konrad Slind, Alan Bundy, Michael J. C. Gordon:
An Interface between Clam and HOL. 87-104 - James L. Caldwell
:
Classical Propositional Decidability via Nuprl Proof Extraction. 105-122 - W. O. David Griffioen, Marieke Huisman
A Comparison of PVS and Isabelle/HOL. 123-142 - Elsa L. Gunter:
Adding External Decision Procedures to HOL90 Securely. 143-152 - John Harrison:
Formalizing Basic First Order Model Theory. 153-170 - John Harrison:
Formalizing Dijkstra. 171-188 - Peter V. Homeier, David F. Martin:
Mechanical Verification of Total Correctness through Diversion Verification Conditions. 189-206 - Douglas J. Howe:
A Type Annotation Scheme for Nuprl. 207-224 - Paul B. Jackson
Verifying a Garbage Collection Algorithm. 225-244 - Karsten Konrad:
HOT: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux. 245-261 - Chuck C. Liang:
Free Variables and Subexpressions in Higher-Order Meta Logic. 263-276 - Maxim Lifantsev, Leo Bachmair:
An LPO-based Termination Ordering for Higher-Order Terms without lambda-abstraction. 277-293 - Anna Mikhajlova, Joakim von Wright:
Proving Isomorphism of First-Order Logic Proof Systems in HOL. 295-314 - Roderick Moten:
Exploiting Parallelism in Interactive Theorem Provers. 315-330 - Olaf Müller:
I/O Automata and Beyond: Temporal Logic and Abstraction in Isabelle. 331-348 - Wolfgang Naraschewski, Markus Wenzel:
Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic. 349-366 - 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. 367-386 - David Nowak, Jean-René Beauvais, Jean-Pierre Talpin:
Co-inductive Axiomatization of a Synchronous Language. 387-399 - François Puitg, Jean-François Dufourd:
Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling. 401-422 - Rimvydas Ruksenas, Joakim von Wright:
A Tool for Data Refinement. 423-441 - Hajime Sawamura, Daisaku Asanuma:
Mechanizing Relevant Logics with HOL. 443-460 - Friedrich W. von Henke, Stephan Pfab, Holger Pfeifer, Harald Rueß:
Case Studies in Meta-Level Theorem Proving. 461-478 - Mitsuharu Yamamoto, Koichi Takahashi, Masami Hagiya, Shin-ya Nishizaki, Tetsuo Tamai:
Formalization of Graph Search Algorithms and Its Applications. 479-496
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 2024-12-19 22:01 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: