| Invited Papers |
| Verified Lexical Analysis / Tobias Nipkow |
| Extending Window Inference / Joakim von Wright |
| Refereed Papers |
| Program Abstraction in a Higher-Order Logic Framework / Marco Benini ; Sara Kalvala ; Dirk Nowotka |
| The Village Telephone System: A Case Study in Formal Software Engineering / Karthikeyan Bhargavan ; Carl A. Gunter ; Elsa L. Gunter ; Michael Jackson ; Davor Obradovic ; Pamela Zave |
| Generating Embeddings from Denotational Descriptions / Richard J. Boulton |
| An Interface between CLaM and HOL / Richard Boulton ; Konrad Slind ; Alan Bundy ; Mike Gordon |
| Classical Propositional Decidability via Nuprl Proof Extraction / James L. Caldwell |
| A Comparison of PVS and Isabelle/HOL / David Griffioen ; Marieke Huisman |
| Adding External Decision Procedures to HOL90 Securely |
| Formalizing Basic First Order Model Theory / John Harrison |
| Formalizing Dijkstra |
| Mechanical Verification of Total Correctness through |
| Diversion Verification Conditions / Peter V. Homeier ; David F. Martin |
| A Type Annotation Scheme for Nuprl / Douglas J. Howe |
| Verifying a Garbage Collection Algorithm / Paul B. Jackson |
| Hot: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux / Karsten Konrad |
| Free Variables and Subexpressions in Higher-Order Meta Logic / Chuck Liang |
| An LPO-Based Termination Ordering for Higher-Order Terms without ?-Abstraction / Maxim Lifantsev ; Leo Bachmair |
| Proving Isomorphism of First-Order Logic Proof Systems in HOL / Anna Mikhajlova |
| Exploiting Parallelism in Interactive Theorem Provers / Roderick Moten |
| I/O Automata and Beyond: Temporal Logic and Abstraction in Isabelle / Olaf Müller |
| Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic / Wolfgang Naraschewski ; Markus Wenzel |
| On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System / Naren Narasimhan ; Ranga Vemuri |
| Co-inductive Axiomatization of a Synchronous Language / David Nowak ; Jean-Rene Beauvais ; Jean-Pierre Talpin |
| Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling / François Puitg ; Jean-François Dufourd |
| A Tool for Data Refinement / Rimvydas RukÃœenas |
| Mechanizing Relevant Logics with HOL / Hajime Sawamura ; Daisaku Asanuma |
| Case Studies in Meta-Level Theorem Proving / Friedrich W. von Henke ; Stephan Pfab ; Holger Pfeifer ; Harald Rueß |
| Formalization of Graph Search Algorithms and Its Applications / Mitsuharu Yamamoto ; Koichi Takahashi ; Masami Hagiya ; Shin-ya Nishizaki ; Tetsuo Tamai |
| Author Index |
| Invited Papers |
| Verified Lexical Analysis / Tobias Nipkow |
| Extending Window Inference / Joakim von Wright |
図書
