Abstract is missing.
- Click n Prove: Interactive Proofs within Set TheoryJean-Raymond Abrial, Dominique Cansell. 1-24 [doi]
- Formal Specification and Verification of ARM6Anthony C. J. Fox. 25-40 [doi]
- A Programming Logic for Java Bytecode ProgramsClaire L. Quigley. 41-54 [doi]
- Verified Bytecode SubroutinesGerwin Klein, Martin Wildmoser. 55-70 [doi]
- Complete Integer Decision Procedures as Derived Rules in HOLMichael Norrish. 71-86 [doi]
- Changing Data Representation within the Coq SystemNicolas Magaud. 87-102 [doi]
- Applications of Polytypism in Theorem ProvingKonrad Slind, Joe Hurd. 103-119 [doi]
- A Coverage Checking Algorithm for LFCarsten Schürmann, Frank Pfenning. 120-135 [doi]
- Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive DefinitionsDeepak Kapur, Nikita A. Sakhanenko. 136-154 [doi]
- Embedding of Systems of Affine Recurrence Equations in CoqDavid Cachera, David Pichardie. 155-170 [doi]
- Programming a Symbolic Model Checker in a Fully Expansive Theorem ProverHasan Amjad. 171-187 [doi]
- Combining Testing and Proving in Dependent Type TheoryPeter Dybjer, Qiao Haiyan, Makoto Takeyama. 188-203 [doi]
- Reasoning about Proof Search Specifications: An AbstractDale Miller. 204 [doi]
- Program Extraction from Large Proof DevelopmentsLuís Cruz-Filipe, Bas Spitters. 205-220 [doi]
- First Order Logic with Domain ConditionsFreek Wiedijk, Jan Zwanenburg. 221-237 [doi]
- Extending Higher-Order Unification to Support Proof IrrelevanceJason Reed. 238-252 [doi]
- Inductive Invariants for Nested RecursionSava Krstic, John Matthews. 253-269 [doi]
- Implementing Modules in the Coq SystemJacek Chrzaszcz. 270-286 [doi]
- MetaPRL - A Modular Logical EnvironmentJason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, Xin Yu. 287-303 [doi]
- Proving Pearl: Knuth s Algorithm for Prime NumbersLaurent Théry. 304-318 [doi]
- Formalizing Hilbert s Grundlagen in Isabelle/IsarLaura I. Meikle, Jacques D. Fleuriot. 319-334 [doi]
- Using Coq to Verify Java Card Applet Isolation PropertiesJune Andronick, Boutheina Chetali, Olivier Ly. 335-351 [doi]
- Verifying Second-Level Security ProtocolsGiampaolo Bella, Cristiano Longo, Lawrence C. Paulson. 352-366 [doi]