Some Papers by Rob Arthan

This page gives a collection of papers and talks by Rob Arthan on Formal Methods and mechanized theorem proving.

• On Formal Specification of a Proof Tool
• On Free Type Definitions in Z
• Undefinedness in Z: Issues for Specification and Proof (also slides)
• Mechanizing Proof for the Z Toolkit
• Recursive Data Types in Typed Set Theory
• Arithmetic for Z
• Modularity for Z
• Issues for Z Concrete Syntax
• Axioms for Mutually Recursive Free Type Definitions
• Recursive Definiitions in Z
• A Typed Formulation of the Semantics of Z
• Analysis of Compiled Code: A Prototype Formal Model (also slides)
• ClawZ : Control Laws in Z (with Paul Caseley, Colin O'Halloran and Alf Smith)
• An Irrational Construction of R from Z (and some supplementary material and slides)
• Some Mathematical Case Studies in ProofPower-HOL
• Sqrt(2) is not in Q - 3 proofs in ProofPower-HOL
• A Verified Formal Model of a VC Generator (see also ProofPower-Z Examples and particularly Correctness of Imperative Programs )
• Mechanising Mathematical Proof: a Progress Report (slides)
• Reasoning About Linear Systems (slides) (with Ursula Martin, Erik Arne Mathiesen and Paulo Oliva)

All of the papers are in PostScript format.

The slides are in HTML/JPEG format created from LaTeX masters using webify.

Created by  Rob Arthan Last updated: $Date: 2008/03/07 14:05:34 $