| EPSRC Reference: |
GR/H73103/01 |
| Title: |
ALGEBRAIC AND LOGICAL FOUNDATIONS OF FORMAL SOFTWARE DEVELOPMENT |
| Principal Investigator: |
Sannella, Professor D |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Sch of Informatics |
| Organisation: |
University of Edinburgh |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
16 February 1993 |
Ends: |
15 August 1996 |
Value (£): |
119,023
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
To continue the investigation of foundations required to ensure the soundness of practical software development in Extended ML and similar frameworks. Particular topics to be studied are: term rewriting in structured specifications; theorem proving in ASL+; a calculus of algebra fragments; behavioural equivalence; the relationship between ASL+ and systems of type theory; implementing a proof checker for ASL+.Progress:The behavioural semantics of specifications with higher-order formulae as axioms has been studied, leading to a characterisation of behavioural abstraction via behavioural satisfaction of formulae in which the equality symbol is interpreted as indistinguishability, generalising [BHW94]. The fact that higher-order logic is powerful enough to express the indistinguishability relation is used to characterise behavioural satisfaction in terms of ordinary satisfaction, and to develop new methods for reasoning about specifications under behavioural semantics [HS95]. Work is in progress on term rewriting in structured specifications, attempting to provide a categorical version of various modularity results. A detailed study of the formal system of ASL+ is underway, with emphasis on connections with work on type theory in general and subtyping in particular [Asp95a], [Asp95b]. A method has been developed for specifying and implementing abstract data types using constructive type theory [Und95]. An overview of ideas underlying work on the model-theoretic foundations of algebraic specification and formal program development was written [ST95]. [Asp95a] D. Aspinall. Subtyping with singleton types. Proc. 1994 Conf. on Computer Science Logic, Kazimierz. Springer LNCS, to appear (1995).[Asp95b] D. Aspinall. Types, subtypes and ASL+. Proc. 1Oth Workshop on Abstract Datatypes, Santa Margherita Ligure. Springer LNCS, to appear (1995).[BHW94] M. Bidoit, R. Hennicker and M. Wirsing. Behavioural and abstractor specifications. Report LIENS-94-10, Ecole Normale Superieure (1994).[HS95] M. Hoffman and D. Sannella. On behavioural abstraction and behavioural satisfaction in higher-order logic. Proc. TAPSOFT95, Aarhus. Springer LNCS, to appear (1995).[ST95] D. Sannella and A. Tarlecki. Model-theoretic foundations for formal program development: basic concepts and motivation. Submitted for journal publication (1995). [Und95] J. Underwood. Typing abstract data types. Proc. 10th Workshop on Abstract Datatypes, Santa Margherita Ligure. Springer LNCS, to appear (1995).
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.ed.ac.uk |