Abstract is missing.
- JavaCard Program VerificationBart Jacobs. 1-3 [doi]
- View from the Fringe of the Fringe (Joint with CHARME 2001)Steven D. Johnson. 4 [doi]
- Using Decision Procedures with a Higher-Order LogicNatarajan Shankar. 5-26 [doi]
- Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVSAndrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey, Ursula Martin, Sam Owre. 27-42 [doi]
- An Irrational Construction of R from ZR. D. Arthan. 43-58 [doi]
- HELM and the Semantic Math-WebAndrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Irene Schena. 59-74 [doi]
- Calculational Reasoning Revisited (An Isabelle/Isar Experience)Gertrud Bauer, Markus Wenzel. 75-90 [doi]
- Mechanical Proofs about a Non-repudiation ProtocolGiampaolo Bella, Lawrence C. Paulson. 91-104 [doi]
- Proving Hybrid Protocols CorrectMark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu 0003. 105-120 [doi]
- Nested General Recursion and Partiality in Type TheoryAna Bove, Venanzio Capretta. 121-135 [doi]
- A Higher-Order Calculus for CategoriesMario Cáccamo, Glynn Winskel. 136-153 [doi]
- Certifying the Fast Fourier Transform with CoqVenanzio Capretta. 154-168 [doi]
- A Generic Library for Floating-Point Numbers and Its Application to Exact ComputingMarc Daumas, Laurence Rideau, Laurent Théry. 169-184 [doi]
- Ordinal Arithmetic: A Case Study for Rippling in a Higher Order DomainLouise A. Dennis, Alan Smaill. 185-200 [doi]
- Abstraction and Refinement in Higher Order LogicMatt Fairtlough, Michael Mendler, Xiaochun Cheng. 201-216 [doi]
- A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOLSimon J. Gay. 217-232 [doi]
- Representing Hierarchical Automata in Interactive Theorem ProversSteffen Helke, Florian Kammüller. 233-248 [doi]
- Refinement Calculus for Logic Programming in Isabelle/HOLDavid Hemer, Ian J. Hayes, Paul A. Strooper. 249-264 [doi]
- Predicate Subtyping with Predicate SetsJoe Hurd. 265-280 [doi]
- A Structural Embedding of Ocsid in PVSPertti Kellomäki. 281-296 [doi]
- A Certified Polynomial-Based Decision Procedure for Propositional LogicInmaculada Medina-Bulo, Francisco Palomo-Lozano, José A. Alonso-Jiménez. 297-312 [doi]
- Finite Set Theory in ACL2J. Strother Moore. 313-328 [doi]
- The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability)Pavel Naumov, Mark-Oliver Stehr, José Meseguer. 329-345 [doi]
- Formalizing Convex Hull AlgorithmsDavid Pichardie, Yves Bertot. 346-361 [doi]
- Experiments with Finite Tree Automata in CoqXavier Rival, Jean Goubault-Larrecq. 362-377 [doi]
- Mizar Light for HOL LightFreek Wiedijk. 378-394 [doi]