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 |

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 |