2-5pm, June 22, 2007
All are welcome to this meeting of the Scottish Theorem Proving Seminar.
Travel directions to the University of Stirling may be found here. Room 2B74 is on the ground floor of the Cottrell Building (up one floor if entering from Queen's Court) and will be signposted on the day.
There are various options for lunch nearby. On campus, the Macrobert Centre restaurant is very popular and there are also several restaurants run by the University Catering service. Near campus, you can choose from pizza and pasta at Corrieri's or pub lunches at the Meadowpark. Further afield, but still within walking distance of the university, there are several eating places in Bridge of Allan.
For further information about the STP seminar series, go to the main STP seminar website.
| 2:00 | Welcome |
| 2:05 | IsaPlanner's Logic for Theory Level Meta-Variables
Abstract Lucas Dixon, University of Edinburgh |
| 2:40 | An algorithm for deriving mean field equations from large process algebra models
Abstract Chris McCaig, University of Stirling |
| 3:15 | Break |
| 3:50 | A general theory of grounded axiomatisation
Abstract Alison Pease, University of Edinburgh |
| 4:25 | Towards a box calculus for Hierarchical Hume
Abstract Gudmund Grov, Heriot-Watt University |
| 5:00 | Close |
Recent developments in IsaPlanner work towards a lazier approach to formal theory development where definitions and theorems do not need to be fully specified and where proofs may be incomplete. I will give some motivating remarks and describe IsaPlanner's logical foundations which attempt to support this middle-out style of working.
In theoretical biology models often describe systems at the level of the population. This is convenient for further analysis, but has the drawback that information about populations cannot be directly observed. In contrast, models at the level of the individual can be based on direct observation, but only limited algebraic analysis is available. Bridging the gap between these different levels is an important challenge as it allows the derivation of population level models which take into account the individual interactions which are fundamental to the behaviour ofthe population.
Here we present an algorithm which, given an individual based model of a system in the process algebra WSCCS, can produce a system of mean field equations which describe the mean behaviour at the level of the population.
Alison Pease
University of Edinburgh
We talk about the process of discovery and justification of mathematical axioms, and how interaction with a physical world can be used to both generate and evaluate axioms. This idea forms the basis of a grant proposal which we are in the process of submitting.
Hume is a new and novel programming language. The novelty lies in its ability to statically cost the time and space usage. This often requires transforming an expressive representation with undecidable properties into less expressive more decidable representations. Here we outline a calculus which supports this kind of transformation. Our long term aim is to automate the transformation process.