MRG home page · Research · Publications · Projects · Software · People

Scottish Theorem Provers Meeting
@ The University of Edinburgh

23 February 2007

Organisers: Natalia Deringer, Alan Bundy

Location

School of Informatics
Appleton Tower, Room 3.05
Crichton Street
Edinburgh, EH8 9LE
How to get here

Programme

13.00 Lunch in Room 3.16.
Please contact
Natalia Deringer if you intend to come to lunch.
14.00 Laura Meikle A Proof Engineering Approach to Systems Integration


Solving sophisticated mathematical problems using interactive theorem provers (TP) can at times be painstaking. Commonly, this can be linked to the presence of algebraic components which are laborious to manipulate using deduction. Computer algebra systems (CAS) can simplify the proof process by providing powerful algebraic algorithms. By integrating such diverse systems one hopes to create a better mechanised mathematics environment where the user can decide whether to sacrifice a possible small loss in formal correctness for a large gain in productivity. This talk will describe our architecture for integrating the theorem prover Isabelle with QEPCAD. We follow closely with Aspinall's "Proof Engineering" paradigm, where a broker communicates between the TP, CAS and UI. This approach has the benefits of positioning the CAS system near to the user rather than near to the prover, which provides transparency of what is being proved where.It also has the advantage of allowing easy interoperability of many systems.
14.45 Ben Gorry PARTES: Performance Analysis of Real-Time Embedded Systems


Verification of real-time software systems can be expensive in terms of time and resources. Testing has traditionally been the main method for showing correctness of real-time systems. Testing, however, can be a long and time consuming process. Performance modeling techniques allow systems to be analysed for timing behaviour. The Stochastic Petri Net Package (SPNP) facilitates the observation of the sensitivity of a performance model to certain input parameters. Everyday engineers are usually unwilling to adopt formal approaches to correctness because of the overhead associated with developing their knowledge of such techniques. This presentation introduces PARTES, a methodology which guides the extraction of performance models from programs written in an annotated subset of C. The behaviour of these performance models can be used to identify potential areas of concern in a real-time system.
15.30 Coffee in Room 3.16
16.15 Stephane Lengrand A sequent calculus framework for proof synthesis in type theory (joint work with Roy Dyckhoff and James McKinna)

Based on natural deduction, Pure Type Systems (PTS) can express a wide range of type theories. In order to express proof-search in such theories, we introduce the Pure Type Sequent Calculi (PTSC) by enriching a sequent calculus due to Herbelin, adapted to proof-search and strongly related to natural deduction. PTSCs are equipped with a normalisation procedure, adapted from Herbelin's and defined by local rewrite rules as in Cut-elimination, using explicit substitutions. It satisfies Subject Reduction and it is confluent. A PTSC is logically equivalent to its corresponding PTS, and the former is strongly normalising if and only if the latter is. We show how the conversion rules can be incorporated inside logical rules (as in syntax-directed rules for type checking), so that basic proof-search tactics in type theory are merely the root-first application of our inference rules.
17.00 Retire to the bar "Centraal" in West Nicholson Street

Previous STP seminars
For further information please contact: Natalia Deringer