EPSRC Reference: 
GR/J97366/01 
Title: 
SYSTEMATIC PROGRAMMING SEMANTICS 
Principal Investigator: 
Ong, Professor CHL 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer Science 
Organisation: 
University of Oxford 
Scheme: 
Standard Research (PreFEC) 
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 nondeterminism 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 nondeterminism 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. Nondeterminism in a functional setting, in: Proc. 8th Annual IEEE Symposium on Logic and in Computer Science, Computer Society Press, pp.275286, 1993. [2] R. Hasegawa. Relational limits in general polymorphism, The Publications of the Research Institute for Mathematical Sciences 30. [3] R. Hasegawa. Wellordering of algebras and Kruskals theorem, in: Logic, Language and Computation, Lect. Notes in Comput. Sci. 792, pp. 133172, SpringerVerlag 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 nonacademic 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 