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
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
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|