We adopt the untyped imperative object calculus of Abadi and Cardelli as a minimal setting in which to study problems of compilation and program equivalence that arise when compiling object-oriented languages. We present both a big-step and a small-step substitution-based operational semantics for the calculus and prove them equivalent to the closure-based operational semantics given by Abadi and Cardelli. Our first result is a direct proof of the correctness of compilation to a stack-based abstract machine via a small-step decompilation algorithm. Our second result is that contextual equivalence of objects coincides with a form of Mason and Talcott's CIU equivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in our prototype compiler, for statically resolving method offsets. This is the first study of correctness of an object-oriented abstract machine, and of operational equivalence for the imperative object calculus.
The spi calculus is an extension of the pi calculus with constructs for encryption and decryption. This paper develops the theory of the spi calculus, focusing on techniques for establishing testing equivalence, and applying these techniques to the proof of authenticity and secrecy properties of cryptographic protocols.
We introduce the spi calculus, an extension of the pi calculus designed for the description and analysis of cryptographic protocols. We show how to use the spi calculus, particularly for studying authentication protocols. The pi calculus (without extension) suffices for some abstract protocols; the spi calculus enables us to consider cryptographic issues in more detail. We represent protocols as processes in the spi calculus and state their security properties in terms of coarse-grained notions of protocol equivalence.
Needham defines a pure name to be ``nothing but a bit pattern that is an identifier, and is only useful for comparing for identity with other bit patterns---which includes looking up in tables in order to find other information''. In this paper, we argue that pure names are relevant to both security and mobility. Nominal calculi are computational formalisms that include pure names and the dynamic generation of fresh, unguessable names. We survey recent work on nominal calculi with primitives representing location failure, process migration and cryptography, and suggest areas for further work.
We present five axioms of name-carrying lambda-terms identified up to
alpha-conversion---that is, up to renaming of bound variables. We assume
constructors for constants, variables, application and lambda-abstraction.
Other constants represent a function Fv that returns the set of
free variables in a term and a function that substitutes a term for a variable
free in another term. Our axioms are (1) equations relating Fv
and each constructor, (2) equations relating substitution and each
constructor, (3) alpha-conversion itself, (4) unique existence of functions on
lambda-terms defined by structural iteration, and (5) construction of
lambda-abstractions given certain functions from variables to terms. By
building a model from de Bruijn's nameless lambda-terms, we show that our five
axioms are a conservative extension of HOL. Theorems provable from the axioms
include distinctness, injectivity and an exhaustion principle for the
constructors, principles of structural induction and primitive recursion on
lambda-terms, Hindley and Seldin's substitution lemmas and the existence of
their length function. These theorems and the model have been mechanically
checked in the Cambridge HOL system.
Some applications are most easily expressed in a programming language that supports concurrency, notably interactive and distributed systems. We propose extensions to the purely-functional language Haskell that allows it to express explicitly concurrent applications; we call the resulting language Concurrent Haskell. The resulting system appears to be both expressive and efficient, and we give a number of examples of useful abstractions that can be built from our primitives. We have developed a freely-available implementation of Concurrent Haskell, and are now using it as a substrate for a graphical user interface toolkit.
Bisimilarity (also known as `applicative bisimulation') has attracted a good deal of attention as an operational equivalence for lambda-calculi. It approximates or even equals Morris-style contextual equivalence and admits proofs of program equivalence via co-induction. It has an elementary construction from the operational definition of a language. We consider bisimilarity for one of the typed object calculi of Abadi and Cardelli. By defining a labelled transition system for the calculus in the style of Crole and Gordon and using a variation of Howe's method we establish two central results: that bisimilarity is a congruence, and that it equals contextual equivalence. So two objects are bisimilar iff no amount of programming can tell them apart. Our third contribution is to show that bisimilarity soundly models the equational theory of Abadi and Cardelli. This is the first study of contextual equivalence for an object calculus and the first application of Howe's method to subtyping. By these results, we intend to demonstrate that operational methods are a promising new direction for the foundations of object-oriented programming.
We describe the design and use of monadic I/O in Haskell 1.3, the latest revision of the lazy functional programming language Haskell. Haskell 1.3 standardises the monadic I/O mechanisms now available in many Haskell systems. The new facilities allow more sophisticated text-based application programs to be written portably in Haskell. Apart from the use of monads, the main advances over standard Haskell 1.2 are: character I/O based on handles (analogous to ANSI C file pointers), an error handling mechanism, terminal interrupt handling and a POSIX interface. The standard also provides implementors with a flexible framework for extending Haskell to incorporate new language features. In addition to a tutorial description of the new facilities this paper includes a worked example: a monad for combinator parsing which is based on the standard I/O monad.
Operational intuition is central to computer science. These notes introduce functional programmers to operational semantics and operational equivalence. We show how the idea of bisimilarity from CCS may be applied to deterministic functional languages. On elementary operational grounds it justifies equational reasoning and proofs about infinite streams.
Morris-style contextual equivalence---invariance of termination under any context of ground type---is the usual notion of operational equivalence for deterministic functional languages such as FPC (PCF plus sums, products and recursive types). Contextual equivalence is hard to establish directly. Instead we define a labelled transition system for call-by-name FPC (and variants) and prove that CCS-style bisimilarity equals contextual equivalence---a form of operational extensionality. Using co-induction we establish equational laws for FPC. By considering variations of Milner's `bisimulations up to ~' we obtain a second co-inductive characterisation of contextual equivalence in terms of reduction behaviour and production of values. Hence we use co-inductive proofs to establish contextual equivalence in a series of stream-processing examples. Finally, by proving a context lemma we show how Milner's original term-model can be extended to FPC, but in fact our form of bisimilarity supports simpler co-inductive proofs.
We study the longstanding problem of semantics for input/output (I/O) expressed using side-effects. Our vehicle is a small higher-order imperative language, with operations for interactive character I/O and based on ML syntax. Unlike previous theories, we present both operational and denotational semantics for I/O effects. We use a novel labelled transition system that uniformly expresses both applicative and imperative computation. We make a standard definition of bisimilarity and prove it is a congruence using Howe's method.
Next, we define a metalogical type theory M which we may give a denotational semantics to O. M generalises Crole and Pitts' FIX-logic by adding in a parameterised recursive datatype, which is used to model I/O. M comes equipped both with judgements of equality of expressions, and an operational semantics; M itself is given a domain-theoretic semantics in the category CPPO of cppos (bottom-pointed posets with joins of omega chains) and Scott continuous functions. We use the CPPO semantics to prove that the equational theory is computationally adequate for the operational semantics using formal approximation relations. The existence of such relations uses key ideas from Pitts' recent work.
A monadic-style textual translation into M induces a denotational semantics on O. Our final result justifies metalogical reasoning: if the denotations of two O programs are equal in M then the O programs are in fact operationally equivalent.
Co-induction is an important tool for reasoning about unbounded structures. This tutorial explains the foundations of co-induction, and shows how it justifies intuitive arguments about lazy streams, of central importance to lazy functional programmers. We explain from first principles a theory based on a new formulation of bisimilarity for functional programs, which coincides exactly with Morris-style contextual equivalence. We show how to prove properties of lazy streams by co-induction and derive Bird and Wadler's Take Lemma, a well-known proof technique for lazy streams.
We present a new strategy for representing syntax in a mechanised logic. We define an underlying type of de Bruijn terms, define an operation of named lambda-abstraction, and hence inductively define a set of conventional name-carrying terms. The result is a mechanisation of the practice of most authors studying formal calculi: to work with conventional name-carrying notation and substitution, but to identify terms up to alpha-conversion. This strategy falls between most previous works, which either treat bound variable names literally or dispense with them altogether. The theory has been implemented in the Cambridge HOL system and used in an experimental application.
This paper contributes to the methodology of using metalogics for reasoning about programming languages. As a concrete example we consider a fragment of ML corresponding to call-by-value PCF and translate it into a metalogic which contains (amongst other types) computation types and a fixpoint type. The main result is a soundness property (*): if the denotations of two programs are provably equal in the metalogic, they have the same operationally observable behaviour. As usual, this follows from a computational adequacy result. In early notes, Plotkin showed how such proofs could be factored into two stages, the first non-trivial and the second (essentially) routine; our contribution is to rework his suggestion within a new framework. We define a metalogic, which incorporates computation and fixpoint types, and specify a modular translation of the ML fragment. Our proof of (*) factors into two parts. First, the term language of the metalogic is equipped with an operational semantics and a (generic) computational adequacy result obtained. Second, a simple syntactic argument establishes a correspondence between the operational behaviour of an object program and of its denotation. The first part is not routine but is proved once and for all. The second is a detailed but essentially trivial calculation that is easily adaptable to other object languages. Such a factored proof is important because it promises to scale up more easily than a monolithic one. We show that it may be adapted to an object language with call-by-name functions and one with a simple exception mechanism.
I/O mechanisms are needed if functional languages are to be suitable for general purpose programming and several implementations exist. But little is known about semantic methods for specifying and proving properties of lazy functional programs engaged in I/O. As a step towards formal methods of reasoning about realistic I/O we investigate three widely implemented mechanisms in the setting of teletype I/O: synchronised-stream (primitive in Haskell), continuation-passing (derived in Haskell) and Landin-stream I/O (where programs map an input stream to an output stream of characters). Using methods from Milner's CCS we give a labelled transition semantics for the three mechanisms. We adopt bisimulation equivalence as equality on programs engaged in I/O and give functions to map between the three kinds of I/O. The main result is the first formal proof of semantic equivalence of the three mechanisms, generalising an informal argument of the Haskell committee.
The Binomial Theorem in HOL is a medium sized worked example whose subject matter is more widely known than any specific piece of hardware or software. This article introduces the small amount of algebra and mathematical notation needed to state and prove the Binomial Theorem, shows how this is rendered in HOL, and outlines the structure of the proof.
If formal methods of hardware verification are to have any impact on the practices of working engineers, connections must be made between the languages used in practice to design circuits, and those used for research into hardware verification. Silage is a simple dataflow language marketed for specifying digital signal processing circuits. Higher Order Logic (HOL) is extensively used for research into hardware verification. This paper presents a formal definition of a substantial subset of Silage, by mapping Silage declarations into HOL predicates. The definition has been mechanised in the HOL theorem prover to support the transformational design of Silage circuits as theorem proving in HOL.
The semantics of hardware description languages can be represented in higher order logic. This provides a formal definition that is suitable for machine processing. Experiments are in progress at Cambridge to see whether this method can be the basis of practical tools based on the HOL theorem-proving assistant. Three languages are being investigated: ELLA, Silage and VHDL. The approaches taken for these languages are compared and current progress on building semantically-based theorem-proving tools is discussed.
If formal methods of hardware verification are to have any impact on the practices of working designers, connections must be made between the languages used in practice to design circuits, and those used for research into hardware verification. Silage is a simple dataflow language used for specifying digital signal processing circuits. Higher Order Logic (HOL) is extensively used for research into hardware verification. We have used a novel combination of operational and predicative semantics to define formally a substantial subset of Silage by mapping Silage definitions into HOL predicates. Here we sketch the method used, discuss what is gained by a formal definition, and explain an immediate practical application---secure transformational design of Silage circuits as theorem proving in HOL.
A common attraction to functional programming is the ease with which proofs can be given of program properties. A common disappointment with functional programming is the difficulty of expressing input/output (I/O) while at the same time being able to verify programs. In this dissertation we show how a theory of functional programming can be smoothly extended to admit both an operational semantics for functional I/O and verification of programs engaged in I/O.
The first half develops the operational theory of a semantic metalanguage used in the second half. The metalanguage M is a simply-typed lambda-calculus with product, sum, function, lifted and recursive types. We study two definitions of operational equivalence: Morris-style contextual equivalence, and a typed form of Abramsky's applicative bisimulation. We prove operational extensionality for M---that these two definitions give rise to the same operational equivalence. We prove equational laws that are analogous to the axiomatic domain theory of LCF and derive a co-induction principle.
The second half defines a small functional language, H, and shows how the semantics of H can be extended to accommodate I/O. H is essentially a fragment of Haskell. We give both operational and denotational semantics for H. The denotational semantics uses M in a case study of Moggi's proposal to use monads to parameterise semantic descriptions. We define operational and denotational equivalences on H and show that denotational implies operational equivalence. We develop a theory of H based on equational laws and a co-induction principle.
We study simplified forms of four widely-implemented I/O mechanisms: side-effecting, Landin-stream, synchronised-stream and continuation-passing I/O. We give reasons why side-effecting I/O is unsuitable for lazy languages. We extend the semantics of H to include the other three mechanisms and prove that the three are equivalent to each other in expressive power.
We investigate monadic I/O, a high-level model for functional I/O based on Wadler's suggestion that monads can express interaction with state in a functional language. We describe a simple monadic programming model, and give its semantics as a particular form of state transformer. Using the semantics we verify a simple programming example.