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.

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

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

Last modified Wednesday 17 October, 2007