Isabelle Users Workshop: Programme
18-19 September 1995
Cambridge, England
All talks to take place in the Hopkinson Lecture Theatre, New
Museums Site, Pembroke Street.
Monday 18 September
- 09.00-09.30
- Registration and Welcome
- 09.30-10.00
- Barendregt's Lambda-Cube in Isabelle
Marco Benini, marco@mirtillo.usr.dsi.unimi.it
- 10.00-10.30
- FS0 in Isabelle:
Adding Structure at the Metalevel
Seán Matthews, sean@mpi-sb.mpg.de
- 10.30-11.00
- Coffee
- 11.00-11.30
- Coding Binding and Substitution
Explicitly in Isabelle
Chris Owens, cao@dcs.edinburgh.ac.uk
- 11.30-12.00
- A Theory of Generic Binding-Structures and
Substitutions
Burkhart Wolff, bu@informatik.uni-bremen.de
- 12.00-14.00
- Lunch (Clare College)
- 14.00-14.30
- Interpretation of the
Deductive Tableau in HOL
Abdelwaheb Ayari and David Basin, {abdu,basin}@mpi-sb.mpg.de
- 14.30-15.00
- Towards program development, specification
and verification with Isabelle
Marek A Bednarczyk and Tomasz Borzyszkowski,
{marek,tomek}@IPIPAN.Gda.PL
- 15.00-15.30
- Miranda in Isabelle
Stephen Hill, Simon Thompson, {S.A.Hill,sjt}@ukc.ac.uk
- 15.30-16.00
- Coffee
- 16.00-16.30
- Combining Model Checking and Deduction
for I/O-Automata
Olaf Müller and Tobias Nipkow,
{mueller,nipkow}@informatik.tu-muenchen.de
- 16.30-17.00
- Ruby in Isabelle
Ole Rasmussen, osr@idatm1.id.dtu.dk
- 17.00-17.30
- A Simple Calculus for
Synthesizing Circuits
David Basin and Stefan Friedrich, {basin,fried}@mpi-sb.mpg.de
Tuesday 19 September
- 09.00-09.30
- A Modular Presentation of Modal Logics
in a Logical Framework
David Basin, Séan Matthews and
Luca Viganò, {basin,sean,luca}@mpi-sb.mpg.de
- 09.30-10.00
- Linear Logic
in Isabelle
Sara Kalvala and Valeria de Paiva, {sk,vcvp}@cl.cam.ac.uk
- 10.00-10.30
- Implementing PPC, a 3-Valued Logic
Dirk Van Heule, dvheule@mmww.rma.ac.be
- 10.30-11.00
- Coffee
- 11.00-11.30
- A Comparison of HOL-ST and Isabelle/ZF
Sten Agerholm, sas@daimi.aau.dk
- 11.30-12.00
- Mechanising Set Theory: Cardinal Arithmetic and
the Axiom of Choice
Larry Paulson, lcp@cl.cam.ac.uk and
Krzysztof Grąbczewski, kgrabcze@mat.uni.torun.pl
- 12.00-14.00
- Lunch (Clare College)
- 14.00-14.30
- Annotation issues in Isabelle
Sara Kalvala, sk@cl.cam.ac.uk
- 14.30-15.00
- Structured Presentation of Formal Proofs --
Experiments with Isabelle
Florian Kammüller, Gabi Keller, Martin Simons and Matthias Weber,
{zopotrum,keller,simons,we}@cs.tu-berlin.de
- 15.00-15.30
- Window Inference in Isabelle
Mark Staples, ms204@cl.cam.ac.uk
- 15.30-16.00
- Coffee
- 16.00-16.30
- On the Representation of Datatypes
in Isabelle/HOL
Norbert Völker, Norbert.Voelker@FernUni-Hagen.de
- 16.30-17.00
- Discussion: the future of Isabelle
- 17.00
- Close
Back to the Isabelle Workshop page
Last modified Wednesday
17 October, 2007
Lawrence C. Paulson • Computer Laboratory • University of Cambridge