Abstract is missing.
- Translating Specifications in VDM-SL to PVSSten Agerholm. 1-16
- A Comparison of HOL and ALF Formalizations of a Categorical Coherence TheoremSten Agerholm, Ilya Beylin, Peter Dybjer. 17-32
- Modeling a Hardware Synthesis Methodology in IsabelleDavid A. Basin, Stefan Friedrich. 33-50
- Inference Rules for Programming Languages with Side Effects in ExpressionsPaul E. Black, Phillip J. Windley. 51-60
- Deciding Cryptographic Protocol Adequacy with HOL: The ImplementationStephen H. Brackin. 61-76
- Proving Liveness of Fair Transition SystemsHolger Busch. 77-92
- Program Derivation Using the Refinement CalculatorMichael J. Butler, Thomas Långbacka. 93-108
- A Proof Tool for Reasoning About Functional ProgramsGraham Collins. 109-124
- Coq and Hardware Verification: A Case StudySolange Coupet-Grimal, Line Jakubiec. 125-139
- Elements of Mathematical Analysis in PVSBruno Dutertre. 141-156
- Implementation Issues About the Embedding of Existing High Level Synthesis Algorithms in HOLDirk Eisenbiegler, Christian Blumenröhr, Ramayya Kumar. 157-172
- Five Axioms of Alpha-ConversionAndrew D. Gordon, Thomas F. Melham. 173-190
- Set Theory, Higher Order Logic or Both?Michael J. C. Gordon. 191-201
- A Mizar Mode for HOLJohn Harrison. 203-220
- Stålmarck s Algorithm as a HOL Derived RuleJohn Harrison. 221-234
- Towards Applying the Composition Principle to Verify a Microkernel Operating SystemMark Heckman, Cui Zhang, Brian R. Becker, Dave Peticolas, Karl N. Levitt, Ronald A. Olsson. 235-250
- A Modular Coding of UNITY in COQBarbara Heyd, Pierre Crégut. 251-266
- Importing Mathematics from HOL into NuprlDouglas J. Howe. 267-281
- A Structure Preserving Encoding of Z in Isabelle/HOLKolyang, Thomas Santen, Burkhart Wolff. 283-298
- Improving the Result of High-Level Synthesis Using Interactive Transformational DesignMats Larsson. 299-314
- Using Lattice Theory in Higher Order LogicLinas Laibinis. 315-330
- Formal Verification of Algorithm W: The Monomorphic CaseDieter Nazareth, Tobias Nipkow. 331-345
- Verification of Compiler Correctness for the WAMCornelia Pusch. 347-361
- Synthetic Domain Theory in Type Theory: Another Logic of Computable FunctionsBernhard Reus. 365-380
- Function Definition in Higher-Order LogicKonrad Slind. 381-397
- Higher-Order Annotated Terms for Proof SearchAlan Smaill, Ian Green. 399-413
- A Comparison of MDG and HOL for Hardware VerificationSofiène Tahar, Paul Curzon. 415-430
- A Mechanisation of Computability Theory in HOLVincent Zammit. 431-446