11. TPHOLs 1998:
Canberra, Australia
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.
Lecture Notes in Computer Science 1479 Springer 1998, ISBN 3-540-64987-5 
Invited Papers
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 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
Last update Wed Feb 15 05:19:23 2012
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
