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)
• Building a Library of Mechanized Mathematical Proofs (slides) (PDF, PostScript)
• Now f is continuous (exercise!) (slides) (PDF)
• HOL Constant Definition Done Right (PDF)

Some of the earlier slideshows are in HTML/JPEG format created from LaTeX masters using a now lost program called webify.

Created by  Rob Arthan Last updated: $Date: 2010/09/05 14:00:24 $