| EPSRC Reference: |
GR/J97366/01 |
| Title: |
SYSTEMATIC PROGRAMMING SEMANTICS |
| Principal Investigator: |
Ong, Professor CHL |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Oxford |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 February 1994 |
Ends: |
31 July 1996 |
Value (£): |
108,299
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
This project contains two closely related research programmes in the semantics of programming languages. One programme is intended to achieve a systematic synthesis of the three dominant techniques (viz. denotational, operational and axiomatic) commonly used in programming language semantics based on a unifying notion of computational types. The other, a major case study, is to develop a functional theory of non-determinism and concurrency.Progress:The second programme identified in the research plan has been completed.The pure untyped lambda calculus augmented by an erratic choice operator and a parallel combinator has been introduced as a vehicle for studying non-determinism and concurrency in the function paradigm following the systematic approach advocated by the project. This work [1] may be seen as a step towards a reapprochement between the algebraic theory of processes in concurrency on the one hand, and the lazy lambda calculus as a foundation for functional programming on the other.The foundational aspects of this project (programme one) have so far concentrated on analyses of the property of parametricity (of types).Many computational types encountered in the semantics of programming languages are generated by simple schema which are compositional. In this vein parametric polymorphism (System F) arises naturally, since many such schema are represented in terms of appropriate compositions of simple constructs which are endowed with both logical and categorical meanings. In [1] we use category theory to explain why parametricity makes representation by system F work correctly. In [3] we show that parametricity also supplies the logical reasoning for the representation. In [2] we examine a simple fragment of computational types and show that it is already powerful enough for proving termination of programs by well (partial) orders, with new combinatorial and logical results. References: [1] C.-H. L. Ong. Non-determinism in a functional setting, in: Proc. 8th Annual IEEE Symposium on Logic and in Computer Science, Computer Society Press, pp.275-286, 1993. [2] R. Hasegawa. Relational limits in general polymorphism, The Publications of the Research Institute for Mathematical Sciences 30. [3] R. Hasegawa. Well-ordering of algebras and Kruskals theorem, in: Logic, Language and Computation, Lect. Notes in Comput. Sci. 792, pp. 133-172, Springer-Verlag 1994. [4] R. Hasegawa. A logical aspect of parametric polymorphism, to appear.
|
|
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.ox.ac.uk |