Abstract is missing.
- Fix-Point Equations for Well-Founded Recursion in Type TheoryAntonia Balaa, Yves Bertot. 1-16
- Programming and Computing in HOLBruno Barras. 17-37
- Proof Terms for Simply Typed Higher Order LogicStefan Berghofer, Tobias Nipkow. 38-52
- Routing Information Protocol in HOL/SPINKarthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic. 53-72
- Recursive Families of Inductive TypesVenanzio Capretta. 73-89
- Aircraft Trajectory Modeling and Altering Algorithm VerificationVictor Carreño, César Muñoz. 90-105
- Intel s Formal Verification Experience on the Willamette DevelopmentRobert P. Colwell, Bob Brennan. 106-107
- A Prototype Proof Translator from HOL to CoqEwen Denney. 108-125
- Proving ML Type Soundness Within CoqCatherine Dubois. 126-144
- On the Mechanization of Real Analysis in Isabelle/HOLJacques D. Fleuriot. 145-161
- Equational Reasoning via Partial ReflectionHerman Geuvers, Freek Wiedijk, Jan Zwanenburg. 162-178
- Reachability Programming in HOL98 Using BDDsMichael J. C. Gordon. 179-196
- Transcendental Functions and Continuity Checking in PVSHanne Gottliebsen. 197-214
- Verified Optimizations for the Intel IA-64 ArchitectureJim Grundy. 215-232
- Formal Verification of IA-64 Division AlgorithmsJohn Harrison. 233-251
- Fast Tactic-Based Theorem ProvingJason Hickey, Aleksey Nogin. 252-267
- Implementing a Program Logic of Objects in a Higher-Order Logic Theorem ProverMartin Hofmann, Francis Tang. 268-282
- A Strong and Mechanizable Grand LogicM. Randall Holmes. 283-300
- Inheritance in Higher Order Logic: Modeling and ReasoningMarieke Huisman, Bart Jacobs. 301-319
- Total-Correctness Refinement for Sequential Reactive SystemsPaul B. Jackson. 320-337
- Divider Circuit Verification with Model Checking and Theorem ProvingRoope Kaivola, Mark Aagaard. 338-355
- Specification and Verification of a Steam-Boiler with Signal-CoqMickaël Kerboeuf, David Nowak, Jean-Pierre Talpin. 356-371
- Functional Procedures in Higher-Order LogicLinas Laibinis, Joakim von Wright. 372-387
- Formalizing Stålmarck s Algorithm in CoqPierre Letouzey, Laurent Théry. 388-405
- TAS - A Generic Window Inference SystemChristoph Lüth, Burkhart Wolff. 406-423
- Weak Alternating Automata in Isabelle/HOLStephan Merz. 424-441
- Graphical Theories of Interactive Systems: Can a Proof Assistant Help?Robin Milner. 442
- Formal Verification of the Alpha 21364 Network ProtocolAbdel Mokkedem, Tim Leonard. 443-461
- Dependently Typed Records for Representing Mathematical StructureRobert Pollack. 462-479
- Towards a Machine-Checked Java Specification BookBernhard Reus, Tatjana Hein. 480-497
- Another Look at Nested RecursionKonrad Slind. 498-518
- Automating the Search for Answers to Open QuestionsLarry Wos, Branden Fitelson. 519-525
- Appendix: Conjectures Concerning Proof, Design, and VerificationLarry Wos. 526-533