Rod Burstall - personal page

I retired in April 2000 as an Emeritus Professor and read my University email only infrequently. Please excuse slow replies.

I am living mostly in France and visit Edinburgh University from time to time. My private mail address - not for circulars please - is

Rod Burstall

Lageas

87700 St Yrieix-sous-Aixe, France

email: rb@dcs.ed.ac.uk. Read infrequently.

Interests: Programming languages, Computation Theory, Computer assisted proof, Type Theory

Personal Interests: Buddhism

Research

Computer assisted proof

We had a research team working on proof using Type Theory. We developed the Lego proof system, and we worked on topics including verifying imperative programs and real time garbage collectors (with Harlequin Plc).

A small proof system - ProveEasy

This is a simple natural deduction proof editor. It was written for student use in the above CS3 course. It is logic independent, but currently has first order logic with equality and some induction.

It was inspired by Lego and Coq, but it does not require understanding of Type Theory.

It is written in Tcl_Tk.

ProveEasy Tcl-Tk code version18 (needs wish8.0), as a gzip'd UNIX tar archive or a plain tar archive.
If you want to use ProveEasy on a Wintel system, you may find the following easier: WinZip'd archive or gzip'd UNIX tar archive.
Documentation is included in version 18, however those of the Wintel persuasion may prefer the M$ Word version of the manual.
ProveEasy Tcl-Tk code version16 (needs wish8.0), as a gzip'd UNIX tar archive or a plain tar archive.

If you have problems downloading any of these files, please e-mail Tim Heap <timh@dcs.ed.ac.uk> for help.

There is a paper about it for the CafeOBJ Symposium, Numazu, Japan April 1998 Teaching people to write Proofs: a Tool

Papers

Burstall, R.M. (1999) Christopher Strachey: Understanding Programming Languages (Draft version) To appear in a special issue of Higher-Order and Symbolic Computation.

Sato M., Sakurai T. and Burstall R. (1999) Explicit Environments, TLCA

Personal material

Some information about Buddhist teaching and practice

Personal material www personal files