EPSRC logo

Details of Grant 

EPSRC Reference: GR/J97366/01
Title: SYSTEMATIC PROGRAMMING SEMANTICS
Principal Investigator: Ong, Professor CHL
Other Investigators:
Pitts, Professor AM
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