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 (minutes available)
17.00
Close

Back to the Isabelle Workshop page


Last modified Wednesday 17 October, 2007


Lawrence C. PaulsonComputer LaboratoryUniversity of Cambridge