Reasoning About CBV Functional Programs in (2008)
We consider the old problem of proving that a computer program meets some specification. By proving, we mean machine checked proof in some formal logic.
IGR Report on EPSRC Grant GR/L89532: Notions of computability for general datatypes (2007)
Mike Fourman, Gordon Plotkin, John Longley
general international e#ort to develop mathematical and conceptual tools suitable for understanding the semantics and logic of a variety of programming languages. The long-term goals of this research...
Note: The current contents of this section are imported from the draft paper [Lon99b]; they are not yet integrated into the present paper. [Explain motivation. Shift in perspective at this point in...
Notions of computability at higher types I (2005)
We discuss the conceptual problem of identifying the natural notions of computability at higher types (over the natural numbers). We argue for an eclectic approach, in which one considers a wide...
Notions of computability at higher types II (2001)
In Part I of this series of papers [Lon01a] we gave a historical survey of the study of notions of higher-type computability. In the present paper and its sequel [Lon01b], we undertake a more...
Constructive Data Refinement in Typed Lambda Calculus (2000)
Furio Honsell, John Longley, Donald Sannella, Andrzej Tarlecki
. A new treatment of data refinement in typed lambda calculus is proposed, based on pre-logical relations [HS99] rather than logical relations as in [Ten94], and incorporating a constructive element....
Constructive Data Refinement in Typed Lambda Calculus (2000)
Furio Honsell, John Longley, Donald Sannella, Andrzej Tarlecki
. A new treatment of data refinement in typed lambda calculus is proposed, phrased in terms of pre-logical relations [HS99] rather than logical relations, and incorporating a constructive element....
Constructive data refinement in typed lambda calculus (2000)
Furio Honsell, John Longley, Donald Sannella, Andrzej Tarlecki
Abstract. A new treatment of data refinement in typed lambda calculus is proposed, phrased in terms of pre-logical relations [HS99] rather than logical relations, and incorporating a constructive...
When is a Functional Program Not a Functional Program? (1999)
In an impure functional language, there are programs whose behaviour is completely functional (in that they behave extensionally on inputs), but the functions they compute cannot be written in the...
Realizability Models for Sequential Computation (1998)
We give an overview of some recently discovered realizability models that embody notions of sequential computation, due mainly to Abramsky, Nickau, Ong, Streicher, van Oosten and the author. Some of...
Logical full abstraction and PCF (1997)
We introduce the concept of logical full abstraction, generalising the usual equational notion. We consider the language PCF and two extensions with “parallel ” operations. The main result is...
Logical Full Abstraction and PCF (1996)
ion and PCF John Longley Gordon Plotkin March 15, 1996 Abstract We introduce the concept of logical full abstraction, generalising the usual equational notion. We consider the language PCF and two...