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