Email Gateway (Aug 18 2022 at 10:35): Email Gateway (Aug 18 2022 at 10:35):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Call for Participation: The Isabelle Workshop 2007
In CADE'07, Bremen, Germany, 16th July 2007.
http://homepages.inf.ed.ac.uk/ldixon/events/isabelle-ws-07/
Overview:
This workshop aims to provides an overview of ongoing developments in
Isabelle for both researchers interested in knowing more about the
system as well Isabelle's developers and users. With the increasing use
of the system and its combination of many automated deduction
techniques, it is important to foster collaboration between different
researchers. For the developers of Isabelle, meeting users is an
important part of focusing development of the system. The workshop will
also provide a forum to discuss new technologies and see a wide range of
applications for automated reasoning. Discussion of formal theory
developments also gives a chance to share knowledge and encourage
improvements to the underlying proof tools and definitional machinery.
Most formalisations in Isabelle's are in Higher-Order Logic, but we also
encourage discussion of developments in other logics.
To register for this workshop and/or the CADE-21 Conference, visit:
http://www.cadeconference.org/meetings/cade21/registration.html
Principal goals of the workshop:
Themes:
Programme:
There will be a programme of short talks and demonstrations and a bound
collection of the abstracts will be circulated to participants and made
available online. The programme will consist of the following
presentations:
(Invited Talk) Makarius Wenzel. "Local proofs, local theories, and
local everything"
Clément Hurlin, Amine Chaieb, Pascal Fontaine, Stephan Merz and Tjark
Weber. "Practical Proof Reconstruction for First-order Logic and
Set-Theoretical Constructions"
Paolo Torrini, Christoph Lüth, Christian Maeder and Till Mossakowski.
"Translating from Haskell to Isabelle"
Harald Hiss. "Checking XML-Specifications"
David Aspinall. "Introducing Proof General Eclipse"
Clemens Ballarin. "Overview of Locales"
Alexander Krauss. "Defining Recursive Functions in Isabelle/HOL 2007"
Stefan Berghofer. "Nominal datatypes in Isabelle/HOL"
Moa Johansson. "Proof Critics for IsaPlanner"
Priya Gopalan. "Concurrent/Distributed theorem proving in
Isabelle/IsaPlanner"
Amine Chaieb. "Integration of local and reflective proof-procedures"
If you have any questions, please email Lucas Dixon:
ldixon@inf.ed.ac.uk
We look forward to seeing you all in Bremen,
The Isabelle workshop organisers,
Lucas Dixon, Moa Johansson
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.7 (GNU/Linux)
Comment: Using GnuPG with Fedora - http://enigmail.mozdev.org
iD8DBQFGdouuiUn2r+81A2gRAvwiAJ0ZehV0Cracdn7v6Modo2gYLbel6wCfYa5+
quTHWIYEr048eecECk/0CkY=
=tuJ6
-----END PGP SIGNATURE-----
Last updated: May 03 2024 at 04:19 UTC