Details of Grant 

EPSRC Reference:	GR/J84205/01
Title:	FRAMEWORKS FOR PROGRAMMING LANGUAGE SEMANTICS AND LOGIC
Principal Investigator:	Plotkin, Professor G
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	Sch of Informatics
Organisation:	University of Edinburgh
Scheme:	Standard Research (Pre-FEC)
Starts:	01 June 1995	Ends:	30 November 1998	Value (£):	321,496
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Related Grants:
Panel History:
Summary on Grant Application Form
We seek frameworks for the syntax, semantics and logic of programming languages, as a scientific basis for constructing complex (distributed) systems. We will consider type-theoretical and categorical approaches to the abstract syntax of programming languages, considering binding operators, general type theory, static semantics, syntax-directed translation, compositional semantics.Classical domain theory concerns typed lambda-calculus, with value and type recursion. We will investigate abstract domain theory and corresponding partial or linear type theories; we seek a representation theorem. We will develop concrete domain theory via enriched functional semantics, treating continuity, stability, perhaps sequentially.The monadic approach concerns notion such as state, exceptions, complexity, non-determinism. We will consider linear type theory for symmetric monads, a two-category variation for non-symmetry, axiomatic treatments of such notions as (probabilistic) non-determinism, complexity.Second-order lambda-calculus models polymorphism and abstract data-types. We will add recursion, notions of computation and subtypes, using second-order linear logic. Classical linear logic may help unify semantics and concurrency. We will investigate trace equivalencies, perhaps weak equivalencies.The logic of computable functions concerns classical domain theory. We will incorporate notions of computation, second-order features; and formulate general correctness logics hoping to reconcile logic of concurrency.
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