Programme

Talks should be 20 Minutes with 10 minutes for questions. Note the long lunch break - this is to give participants time to explore the countryside around The Burn..

Day 1: Wed 4th April

09:00 -- 09:30 Breakfast
Session 1: Induction and Related Methods
09:45 -- 10:15 Moa Johansson Lemma Speculation in Higher-order logic
10:15 -- 10:45 Andrew Ireland A Cooperative Approach to Loop Invariant Discovery for Pointer Programs
We propose a cooperative approach to reasoning about the correctness of pointer programs within the context of separation logic. A key hurdle to achieving scalable program proof is the burden imposed by the need for loop invariants. Pointer data structures can be viewed in terms of their shape and content. Our proposal exploits this distinction by combining two techniques for automating the discovery of loop invariants. Firstly, a technique developed at CMU for discovering shape invariants based upon symbolic evaluation. Secondly, middle-out proof planning, a theorem proving technique applicable to reasoning about loops and which supports loop invariant discovery. We believe that the complementary nature of these techniques will deliver significant advantages in terms of scalable pointer program proof.
10:45 -- 11:15 Markus Aderhold Improvements in Formula Generalization
For proofs by induction it is often necessary to generalize statements to strengthen the induction hypotheses. We present improved heuristics to generalize away subterms, unnecessary conditions and function symbols in a formula. This resolves shortcomings that we encountered within an experimental evaluation of generalization heuristics from the literature. Our generalization method has been implemented in the verification tool VeriFun. An evaluation with examples from the literature as well as several case studies of our own demonstrates the success of the improvements.
11:15 -- 11:30 Coffee
Session 2: User Interfaces
11:30 -- 12:00 David Aspinall and Christoph Lüth Beyond Script Management
12:00 -- 12:30 Serge Autexier Enabling Proof Assistance Systems to Provide Services in Texteditors: The Issue of Truth Maintenance
In order to foster the use of proof assistance systems, we integrated the proof assistant OMEGA into the standard scientific text-editor TEXMACS. We aim at a document-centric approach to formalising and verifying mathematics and software, where the author can write her document without any restrictions while being assisted by OMEGA that provides its services inside the text-editor. In order to effectively assist the author, the proof assistance system must be able to maintain as much of the information about checked parts of the document---for instance proof steps---through arbitrary modifications of the document. This requires a sophisticated truth-maintenance system that spans throughout the whole proof assistance system. We present an enhanced combination of development graphs and the proof datastructure as a formal foundation to describe OMEGA's truth maintenance system as well as the support services offered to the author on that basis.
12:30 -- 13:00 Marc Wagner Integrating the Text-Editor TeXmacs with the Proof Assistance System OMEGA using PLATO
We present a generic mediator, called PLATO, between text editors and proof assistants and how it served to integrate the proof assistant OMEGA into TEXMACS. The aim of this mediator is to support the development, formalisation and publication of mathematical documents as naturally as possible. In particular PLATO should allow the user to author his mathematical documents with a scientific WYSIWYG text editor in the informal language he is used to, that is a mixture of natural language and formulas. These documents can be semantically annotated preserving the textual structure by using the flexible parameterised proof language which we present. From this informal semantic representation PLATO automatically builds up the corresponding formal representation for a proof assistant, in our case OMEGA. The most important task of the mediator is the maintenance of consistent formal and informal representations during the further development of the document in interaction with OMEGA. The presentation will include a demo of the resulting system.
13:00 -- 15:30 Lunch
Session 3: Security
15:30--16:00 Graham Steel A Formal Theory of Key Conjuring
Key Conjuring is a technqiue used to attack the APIs of tamper proof hardware security modules. We have devised a formal transformtion that takes a set of API rules and determines all the computationally feasible key conjuring operations. This talk will explain what all this means, with plenty of examples.
16:00--16:30 Dietter Hutter Preserving Privacy in Web Services Using Information Flow Control
The vision of a landscape of heterogeneous web services deployed as encapsulated business software assets in the Internet is currently becoming a reality as part of the Semantic Web. When pro-active agents handle the context-aware discovery, acquisition, composition, and management of application services and data, ensuring the security of customers' data becomes a principle task. To dynamically compose its offered service, an agent has to process and spread confidential data to other web services demanding the required degree of security. In this talk we propose a methodology based on type-based information flow to control the privacy of data and their proliferation within a set of communicating web services.
16:30 -- 16:45 Coffee
Session 4: "Real Mathematics"
16:45 -- 17:15 Roy McCasland MATHsAiD: an Update
I will present an update on some of the recent developments with the mathematical theorem discovery system MATHsAiD. In particular, I will talk about the re-designed hypothesis generator and the new higher order capabilities of the system. A brief demo will also be given.
17:15 -- 17:45 CP Wirth Ceterum censeo Descente Infinie esse disputandam
We try to give a possible explanation for the popular erroneous believe that explicit induction is crucial for the automation of inductive proofs. We present the only proof of Pierre Fermat by descente infinie that is known to exist today. We present a self-contained proof in a modern form, which nevertheless is intended to follow Fermat's ideas as interpreted into the cited Latin original. We then annotate an English translation of Fermat's original proof with terms from the modern proof. We offer to discuss descente infinie from the mathematical, logical, historical, linguistic, and refined logic-historical points of view.
17:45 -- 18:15 Alison Pease Lakatos-style reasoning for axiom selection and modification
Lakatos outlined a theory of how mathematical progress may occur. We consider how this theory may be applied to the selection and modification of axioms in set theory and geometry.
18:30 Bar opens
19:00 Dinner
22:00 Bar closes

Day 2: Thu 5th April

09:00 -- 09:30 Breakfast
Session 5: Representation and Reasoning
09:45--10:15 Dominik Dietrich What comes above the Assertion Level?
I give an overview about the current state of the omega prover. Starting from inferences, which are the atomic proof building blocks in omega and work directly at the assertion level, we will reach the concept of a strategy, which is the main concept for performing search. Finally I present ideas of how to organize search at the strategy level which I want to discuss with you during the week in Scotland.
10:15 -- 10:45 Fiona McNeill Structural Semantic Matching
10:45 -- 11:15 Alan Bundy Towards a Theory of Ontology Repair or Truthfulness Considered Harmful
We give a formal definition of the problem of ontology repair and are working towards formal definitions of some ontology repair operations. We note that truthfulness in an ontology repair operation is an undesirable property as it makes it difficult, if not impossible, then to use it for ontology repair. To avoid truthfulness, and related problems of inconsistency and definitional vagueness, in the straightforward syntactic definitions of these repair operations, we are experimenting with semantic alternatives. We plan to prove theoretic properties of these semantically defined repair operations and to implement them and evaluate them experimentally.
11:15 -- 11:30 Coffee
Session 6: Theory
11:30 -- 12:00 Alan Smaill Procedural proofs and reflection principles
Several people locally in Edinburgh have made use of inference systems loosely inspired by the constructive omega rule for the natural numbers, which allows a universally quantified statement to be inferred from a suitable effective procedure that generates the proofs of the individual instances. Torkel Franzen suggested that the formalisations used could more accurately be regarded as making use of a proof-theoretic reflection principle over a standard initial logic. I will explain what is involved, and why I think this suggestion is right.
12:00 -- 12:30 Paul Jackson Formal Languages for Mathematics
Most formalised mathematics is hard to read. This talk looks at how to bring the formal language of terms, types and formulas closer to that used in textbooks and papers. After reviewing awkwardnesses of the HOL language, the talk explores richer languages based on more expressive type systems and set theory foundations (e.g. that of the Mizar proof assistant) and makes suggestions for future research in this area.
12:30 -- 13:00 Lucas Dixon Datatype Morphisms
We consider a deep embedding of a restricted class of datatypes (and-or trees) in order to implement some useful morphisms. As an example, we consider the automatic creation of the zipper. This gives two directions for such morphisms: as machinery to support generic programming, and as another class of theory formation.
13:00 -- 14:30 Lunch & CIAO Business Chat