![[Lemma 1]](../lemma1.gif)
|
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, revised 18th April 2014)
-
Mining Human Proofs from Machine Proofs (PDF)
-
Mechanized Mathematical Proof. Why do it? What is it like to do? How are
we getting on with it? (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
![[rda at lemma-one dot com]](../email.gif)
|
|
Last updated: $Date: 2025/03/30 00:09:20 $
|
|
|