Abstract is missing.
- Verified Lexical AnalysisTobias Nipkow. 1-15
- Extending Window InferenceJoakim von Wright. 17-32
- Program Abstraction in a Higher-Order Logic FrameworkMarco Benini, Sara Kalvala, Dirk Nowotka. 33-48
- The Village Telephone System: A Case Study in Formal Software EngineeringKarthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Davor Obradovic, Pamela Zave. 49-66
- Generating Embeddings from Denotational DescriptionsRichard J. Boulton. 67-86
- An Interface between Clam and HOLRichard J. Boulton, Konrad Slind, Alan Bundy, Michael J. C. Gordon. 87-104
- Classical Propositional Decidability via Nuprl Proof ExtractionJames L. Caldwell. 105-122
- A Comparison of PVS and Isabelle/HOLW. O. David Griffioen, Marieke Huisman. 123-142
- Adding External Decision Procedures to HOL90 SecurelyElsa L. Gunter. 143-152
- Formalizing Basic First Order Model TheoryJohn Harrison. 153-170
- Formalizing DijkstraJohn Harrison. 171-188
- Mechanical Verification of Total Correctness through Diversion Verification ConditionsPeter V. Homeier, David F. Martin. 189-206
- A Type Annotation Scheme for NuprlDouglas J. Howe. 207-224
- Verifying a Garbage Collection AlgorithmPaul B. Jackson. 225-244
- HOT: A Concurrent Automated Theorem Prover Based on Higher-Order TableauxKarsten Konrad. 245-261
- Free Variables and Subexpressions in Higher-Order Meta LogicChuck Liang. 263-276
- An LPO-based Termination Ordering for Higher-Order Terms without lambda-abstractionMaxim Lifantsev, Leo Bachmair. 277-293
- Proving Isomorphism of First-Order Logic Proof Systems in HOLAnna Mikhajlova, Joakim von Wright. 295-314
- Exploiting Parallelism in Interactive Theorem ProversRoderick Moten. 315-330
- I/O Automata and Beyond: Temporal Logic and Abstraction in IsabelleOlaf Müller. 331-348
- Object-Oriented Verification Based on Record Subtyping in Higher-Order LogicWolfgang Naraschewski, Markus Wenzel. 349-366
- On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis SystemNaren Narasimhan, Ranga Vemuri. 367-386
- Co-inductive Axiomatization of a Synchronous LanguageDavid Nowak, Jean-René Beauvais, Jean-Pierre Talpin. 387-399
- Formal Specification and Theorem Proving Breakthroughs in Geometric ModelingFrançois Puitg, Jean-François Dufourd. 401-422
- A Tool for Data RefinementRimvydas Ruksenas, Joakim von Wright. 423-441
- Mechanizing Relevant Logics with HOLHajime Sawamura, Daisaku Asanuma. 443-460
- Case Studies in Meta-Level Theorem ProvingFriedrich W. von Henke, Stephan Pfab, Holger Pfeifer, Harald Rueß. 461-478
- Formalization of Graph Search Algorithms and Its ApplicationsMitsuharu Yamamoto, Koichi Takahashi, Masami Hagiya, Shin-ya Nishizaki, Tetsuo Tamai. 479-496