Isabelle logoIsabelle Users Workshop

18-19 September 1995
Cambridge, England

Isabelle users exchanged techniques and results. Both finished work and work in progress were reported. Papers were submitted electronically. There was no formal refereeing.

The workshop was held at the University of Cambridge. Accommodation was in Clare College.

The programme and list of participants are available.

Proceedings: Titles, Abstracts, Papers

A printed proceedings was produced from the papers appearing below. (Most of the titles link to abstracts, not the full papers.)

Front matter (Cover, preface, table of contents)

Framework Issues

Marco Benini, marco@mirtillo.usr.dsi.unimi.it
Barendregt's Lambda-Cube in Isabelle (full paper)

Seán Matthews, sean@mpi-sb.mpg.de
FS0 in Isabelle:
Proceedings paper available

Chris Owens, cao@dcs.edinburgh.ac.uk
Coding Binding and Substitution Explicitly in Isabelle
Proceedings paper available

Set Theory

Sten Agerholm, sas@daimi.aau.dk
A Comparison of HOL-ST and Isabelle/ZF
Proceedings paper available

Larry Paulson, lcp@cl.cam.ac.uk and
Krzysztof GrÄ…bczewski, kgrabcze@mat.uni.torun.pl
Mechanising Set Theory: Cardinal Arithmetic and
Proceedings paper available

Reasoning about Programs

Abdelwaheb Ayari and David Basin, {abdu,basin}@mpi-sb.mpg.de
Interpretation of the Deductive Tableau in HOL
Proceedings paper available

Marek A Bednarczyk and Tomasz Borzyszkowski, {marek,tomek}@IPIPAN.Gda.PL
Towards program development, specification
Proceedings paper available

Stephen Hill, Simon Thompson, sjt@ukc.ac.uk
Miranda in Isabelle
Proceedings paper available

Modal and Linear Logic

David Basin, Sáan Matthews and ò, {basin,sean,luca}@mpi-sb.mpg.de
A Modular Presentation of Modal Logics
Proceedings paper available

Sara Kalvala and Valeria de Paiva, {sk,vcvp}@cl.cam.ac.uk
Linear Logic in Isabelle (full paper)

Proof Presentation

Sara Kalvala, sk@cl.cam.ac.uk
Annotation issues in Isabelle
Proceedings paper available

Florian Kammüller, Gabi Keller, Martin Simons and Matthias Weber, {zopotrum,keller,simons,we}@cs.tu-berlin.de
Structured
Proceedings paper available

Mark Staples, ms204@cl.cam.ac.uk
Window Inference in Isabelle
Proceedings paper available

Isabelle development

Norbert Völker, Norbert.Voelker@FernUni-Hagen.de
On the Representation of Datatypes in Isabelle/HOL
Proceedings paper available

Bo Zheng, zhengb_0@seraph1.sewanee.edu and
lcp@cl.cam.ac.uk
On Linear Decision Procedures

Hardware systems

Olaf Müller and Tobias Nipkow, {mueller,nipkow}@in.tum.de
Combining Model Checking and Deduction for I/O-Automata
Proceedings paper available

Ole Rasmussen, osr@idatm1.id.dtu.dk
Ruby in Isabelle
Proceedings paper available


Last revised: Thursday, 6 October 2022


Lawrence C. PaulsonComputer LaboratoryUniversity of Cambridge