| EPSRC Reference: |
GR/J07303/01 |
| Title: |
FORMAL DEVELOPMENT OF MODULAR PROGRAMS IN EXTENDED ML |
| 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: |
01 July 1993 |
Ends: |
30 September 1996 |
Value (£): |
146,151
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
To continue research on practical formal development of modular Standard ML (SML) programs from Extended ML (EML) specifications. Topics to be studied include: support for proof in EML, including the provision of a prototype proof support tool; the production of one or more substantial case studies in formal development; and research on possible extensions to the EML language and framework.Progress:The full formal semantics of the Extended ML language has been completed [KST94a]. A companion paper presents the main ideas and technicalities of the semantics in a more digestible way [KST95]. A position paper on EML was presented at a workshop on interface definition languages [KST94b]. Work has begun on proof rules for EML that are sound with respect to the interpretation of formulae given in the semantics. Case studies are being written up. A new type-theoretic interpretation of the SML/EML module language is being developed, with the goal of showing that the separation between core and modules language is unnecessary. [KST94a] S. S. Kahrs, D. Sannella and A. Tarlecki. The definition of Extended ML. Report ECS-LFCS-94-300, Laboratory for Foundations of Computer Science, Dept. of Computer Science, Univ. of Edinburgh, 156 pages (1994).[KST94b] S. Kahrs, D. Sannella and A. Tarlecki. Interfaces and Extended ML. Proc. ACM Workshop on Interface Definition Languages, Portland. SIGPLAN Notices 29(8):111-118 (1994).[KST95] S. Kahrs, D. Sannella and A. Tarlecki. The semantics of Extended ML: a gentle introduction. Submitted for journal publication (1995). An earlier version appeared in: Proc. Intl. Workshop on Semantics of Specification Languages, Utrecht, October 1993. Springer Workshops in Computing, 186-215 (1994).
|
|
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 |