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

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

Created by  Rob Arthan Last updated: $Date: 2008/07/11 15:20:13 $