11. TPHOLs 1998: Canberra, Australia

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 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