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.
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)
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
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
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
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)
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
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
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