Abstracts

My papers and publications, in reverse order of publication. A concise list omitting the abstracts is also available.


Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets. Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough (2005). Accepted for SIGCOMM 2005. [Brief].

Abstract:

Network protocols are hard to implement correctly. Despite the existence of RFCs and other standards, implementations often have subtle differences and bugs. One reason for this is that the specifications are typically informal, and hence inevitably contain ambiguities. Conformance testing against such specifications is challenging.

In this paper we present a practical technique for rigorous protocol specification that supports specification-based testing. We have applied it to TCP, UDP, and the Sockets API, developing a detailed `post-hoc' specification that accurately reflects the behaviour of several existing implementations (FreeBSD 4.6, Linux 2.4.20-8, and Windows XP SP1). The development process uncovered a number of differences between and infelicities in these implementations.

Our experience shows for the first time that rigorous specification is feasible for protocols as complex as TCP. We argue that the technique is also applicable `pre-hoc', in the design phase of new protocols. We discuss how such a design-for-test approach should influence protocol development, leading to protocol specifications that are both unambiguous and clear, and to high-quality implementations that can be tested directly against those specifications.

[PDF (360K)].


TCP, UDP, and Sockets: rigorous and experimentally-validated behavioural specification. Volume 1: Overview. Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough (2005). See also related documents on the Network semantics page. [Brief].

Abstract:

We have developed a mathematically rigorous and experimentally-validated post-hoc specification of the behaviour of TCP, UDP, and the Sockets API. It characterises the API and network-interface interactions of a host, using operational semantics in the higher-order logic of the HOL automated proof assistant. The specification is detailed, covering almost all the information of the real-world communications: it is in terms of individual TCP segments and UDP datagrams, though it abstracts from the internals of IP. It has broad coverage, dealing with arbitrary API call sequences and incoming messages, not just some well-behaved usage. It is also accurate, closely based on the de facto standard of (three of) the widely-deployed implementations. To ensure this we have adopted a novel experimental semantics approach, developing test generation tools and symbolic higher-order-logic model checking techniques that let us validate the specification directly against several thousand traces captured from the implementations.

The resulting specification, which is annotated for the non-HOL-specialist reader, may be useful as an informal reference for TCP/IP stack implementors and Sockets API users, supplementing the existing informal standards and texts. It can also provide a basis for high-fidelity automated testing of future implementations, and a basis for design and formal proof of higher-level communication layers. More generally, the work demonstrates that it is feasible to carry out similar rigorous specification work at design-time for new protocols. We discuss how such a design-for-test approach should influence protocol development, leading to protocol specifications that are both unambiguous and clear, and to high-quality implementations that can be tested directly against those specifications.

This document (Volume 1) gives an overview of the project, discussing the goals and techniques and giving an introduction to the specification. The specification itself is given in the companion Volume 2 (UCAM-CL-TR-625), which is automatically typeset from the (extensively annotated) HOL source. As far as possible we have tried to make the work accessible to four groups of intended readers: workers in networking (implementors of TCP/IP stacks, and designers of new protocols); in distributed systems (implementors of software above the Sockets API); in distributed algorithms (for whom this may make it possible to prove properties about executable implementations of those algorithms); and in semantics and automated reasoning.

University of Cambridge Computer Laboratory Technical Report [UCAM-CL-TR-624] [PDF (1263K)].


TCP, UDP, and Sockets: rigorous and experimentally-validated behavioural specification. Volume 2: The specification. Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough (2005). Technical report. [Brief].

Abstract:

See Volume 1 (UCAM-CL-TR-624).

University of Cambridge Computer Laboratory Technical Report [UCAM-CL-TR-625] [PDF (2.4M)].


The TCP Specification: A Quick Introduction. Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough (2004). Unpublished note. [Brief].

[PDF (132K)].


Acute: High-level programming language design for distributed computation: Design rationale and language definition. Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-Williams, Francesco Zappa Nardelli, Pierre Habouzit, Viktor Vafeiadis. (2004). This short paper gives an overview of the main design choices. [Brief].

[PDF (248K)].


Acute: High-level programming language design for distributed computation: Design rationale and language definition. Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-Williams, Francesco Zappa Nardelli, Pierre Habouzit, Viktor Vafeiadis (2004). See also related documents on the Acute home page. [Brief].

Abstract:

This paper studies key issues for distributed programming in high-level languages. We discuss the design space and describe an experimental language, Acute, which we have de ned and implemented.

Acute extends an OCaml core to support distributed development, deployment, and execution, allowing typesafe interaction between separately-built programs. It is expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs, disentangling the language runtime from communication.

This requires a synthesis of novel and existing features: (1) type-safe marshalling of values between programs; (2) dynamic loading and controlled rebinding to local resources; (3) modules and abstract types with abstraction boundaries that are respected by interaction; (4) global names, generated either freshly or based on module hashes: at the type level, as runtime names for abstract types; and at the term level, as channel names and other interaction handles; (5) versions and version constraints, integrated with type identity; (6) local concurrency and thread thunki cation; and (7) second-order polymorphism with a namecase construct. We deal with the interplay among these features and the core, and develop a semantic de nition that tracks abstraction boundaries, global names, and hashes throughout compilation and execution, but which still admits an ef cient implementation strategy.

University of Cambridge Computer Laboratory Technical Report [UCAM-CL-TR-605] [PDF (1155K)].


Applied Semantics: Specifying and Developing Abstractions for Distributed Computation. Peter Sewell, Keith Wansbrough (2004). Discussion paper for UKCRC Grand~Challenges for Computing Research exercise. [Brief].

Abstract: Over the last six years or so much of our research, together with colleagues, has aimed at establishing solid foundations for large-scale distributed computation: applying semantic techniques (existing or newly-developed) to real-world system problems. In this paper we briefly reflect on this work, discussing its relationship to the Grand Challenge proposals
  • GC2: Science for Global Ubiquitous Computing,
  • GC4: Scalable Ubiquitous Computing Systems, and
  • GC6: Dependable systems evolution,
and the conclusions for these that can be drawn from our experience. This paper gives a personal view: we cannot here survey the entire field except in the broadest terms, and so, with apologies to its authors, do not discuss the substantial body of related research.

[PDF (70K)] [PS.GZ (228K)].


Dynamic Rebinding for Marshalling and Update, with Destruct-time lambda. Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, Keith Wansbrough (2003). In International Conference on Functional Programming (ICFP 2003), August 2003, Uppsala, Sweden. [Brief].

Abstract: Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example when a marshalled value is received from the network, containing identifiers that must be rebound to local resources. Typically it is provided only by ad-hoc mechanisms that lack clean semantics.

In this paper we adopt a foundational approach, developing core dynamic rebinding mechanisms as extensions to simply-typed call-by-value lambda-calculus. To do so we must first explore refinements of the call-by-value reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduce redex-time and destruct-time strategies. The latter forms the basis for a lambda-marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically-typed. We sketch an extension of lambda-marsh with concurrency and communication, giving examples showing how wrappers for encapsulating untrusted code can be expressed. Finally, we show that a high-level semantics for dynamic updating can also be based on the destruct-time strategy, defining a lambda-update calculus with simple primitives to provide type-safe updating of running code. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding requirements.

[PS.GZ (594K)].


Dynamic Rebinding for Marshalling and Update, with Destruct-time lambda. Gavin Bierman, Michael Hicks, Peter Sewell, Gareth Stoyle, Keith Wansbrough (2004). Technical report. [Brief].

Abstract: Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises, for example when a marshalled value is received from the network, containing identifiers that must be rebound to local resources. Typically it is provided only by ad-hoc mechanisms that lack clean semantics.

In this paper we adopt a foundational approach, developing core dynamic rebinding mechanisms as extensions to simply-typed call-by-value lambda-calculus. To do so we must first explore refinements of the call-by-value reduction strategy that delay instantiation, to ensure computations make use of the most recent versions of rebound definitions. We introduce redex-time and destruct-time strategies. The latter forms the basis for a lambda-marsh calculus that supports dynamic rebinding of marshalled values, while remaining as far as possible statically-typed. We sketch an extension of lambda-marsh with concurrency and communication, giving examples showing how wrappers for encapsulating untrusted code can be expressed. Finally, we show that a high-level semantics for dynamic updating can also be based on the destruct-time strategy, defining a lambda-update calculus with simple primitives to provide type-safe updating of running code. We thereby establish primitives and a common semantic foundation for a variety of real-world dynamic rebinding requirements.

University of Cambridge Computer Laboratory Technical Report [UCAM-CL-TR-568] [PDF (720K)].


Global Abstraction-Safe Marshalling with Hash Types. James J. Leifer, Gilles Peskine, Peter Sewell, Keith Wansbrough (2003). In International Conference on Functional Programming (ICFP 2003), August 2003, Uppsala, Sweden. [Brief].

Abstract: Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent stores. In this paper we combine the two, developing compile-time and run-time semantics for marshalling, that guarantee abstraction-safety between separately-built programs.

We obtain a namespace for abstract types that is global, i.e., meaningful between programs, by hashing module declarations. We examine the scenarios in which values of abstract types are communicated from one program to another, and ensure, by constructing hashes appropriately, that the dynamic and static notions of type equality mirror each other. We use singleton kinds to express abstraction in the static semantics; abstraction is tracked in the dynamic semantics by coloured brackets. These allow us to prove preservation, erasure, and coincidence results. We argue that our proposal is a good basis for extensions to existing ML-like languages, pragmatically straightforward for language users and for implementors.

[PS.GZ (767K)].


Global Abstraction-Safe Marshalling with Hash Types. James J. Leifer, Gilles Peskine, Peter Sewell, Keith Wansbrough (2004). Technical report. [Brief].

Abstract: Type abstraction is a key feature of ML-like languages for writing large programs. Marshalling is necessary for writing distributed programs, exchanging values via network byte-streams or persistent stores. In this paper we combine the two, developing compile-time and run-time semantics for marshalling, that guarantee abstraction-safety between separately-built programs.

We obtain a namespace for abstract types that is global, i.e., meaningful between programs, by hashing module declarations. We examine the scenarios in which values of abstract types are communicated from one program to another, and ensure, by constructing hashes appropriately, that the dynamic and static notions of type equality mirror each other. We use singleton kinds to express abstraction in the static semantics; abstraction is tracked in the dynamic semantics by coloured brackets. These allow us to prove preservation, erasure, and coincidence results. We argue that our proposal is a good basis for extensions to existing ML-like languages, pragmatically straightforward for language users and for implementors.

University of Cambridge Computer Laboratory Technical Report [UCAM-CL-TR-569] [PDF (762K)].


Rigour is good for you and feasible: reflections on formal treatments of C and UDP sockets. Michael Norrish, Peter Sewell, Keith Wansbrough (2002). In Tenth ACM SIGOPS European Workshop: Can We Really Depend on an OS?, September 2002, Saint-Emilion, France. [Brief].

Abstract: We summarise two projects that formalised complex real world systems. We describe their goals and the techniques used in both. We conclude by discussing how such techniques might be applied to other system software and by describing the benefits this may bring.

[PS.GZ (27K)].


Timing UDP: mechanized semantics for sockets, threads and failures. Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov (2002). In Daniel Le Métayer, ed., European Symposium on Programming (ESOP 2002), Grenoble, April 2002. LNCS 2305. [Brief].

Abstract: This paper studies the semantics of failure in distributed programming. We present a semantic model for distributed programs that use the standard sockets interface; it covers message loss, host failure and temporary disconnection, and supports reasoning about distributed infrastructure. We consider interaction via the UDP and ICMP protocols.

To do this, it has been necessary to: construct an experimentally-validated post-hoc specification of the UDP/ICMP sockets interface; develop a timed operational semantics with threads, as such programs are typically multithreaded and depend on timeouts; model the behaviour of partial systems, making explicit the interactions that the infrastructure offers to applications; integrate the above with semantics for an executable fragment of a programming language (OCaml) with OS library primitives; and use tool support to manage complexity, mechanizing the model with the HOL theorem prover. We illustrate the whole with a module providing naive heartbeat failure detection.

Copyright ©Springer-Verlag. [LNCS 2305] [PS.GZ (111K)] [PDF (264K)].


Simple Polymorphic Usage Analysis. Keith Wansbrough (2002). PhD thesis, Computer Laboratory, University of Cambridge, England. [Brief].

Abstract: Implementations of lazy functional languages ensure that computations are performed only when they are needed, and save the results so that they are not repeated. This frees the programmer to describe solutions at a high level, leaving details of control flow to the compiler.

This freedom however places a heavy burden on the compiler; measurements show that over 70% of these saved results are never used again. A usage analysis that could statically detect values used at most once would enable these wasted updates to be avoided, and would be of great benefit. However, existing usage analyses either give poor results or have been applied only to prototype compilers or toy languages.

This thesis presents a sound, practical, type-based usage analysis that copes with all the language features of a modern functional language, including type polymorphism and user-defined algebraic data types, and addresses a range of problems that have caused difficulty for previous analyses, including poisoning, mutual recursion, separate compilation, and partial application and usage dependencies. In addition to well-typing rules, an inference algorithm is developed, with proofs of soundness and a complexity analysis.

In the process, the thesis develops simple polymorphism, a novel approach to polymorphism in the presence of subtyping that attempts to strike a balance between pragmatic concerns and expressive power. This thesis may be considered an extended experiment into this approach, worked out in some detail but not yet conclusive.

The analysis described was designed in parallel with a full implementation in the Glasgow Haskell Compiler, leading to informed design choices, thorough coverage of language features, and accurate measurements of its potential and effectiveness when used on real code. The latter demonstrate that the analysis yields moderate benefit in practice.

Available from my thesis page. University of Cambridge Computer Laboratory Technical Report [UCAM-CL-TR-623 (with variant pagination)] [PDF (2.3M)] [PS.GZ (2.6M)].


The UDP Calculus: Rigorous Semantics for Real Networking. Andrei Serjantov, Peter Sewell, and Keith Wansbrough (2001). In Theoretical Aspects of Computer Science (TACS2001), October 29-31, 2001, Sendai, Japan. [Brief].

Abstract: Network programming is notoriously hard to understand: one has to deal with a variety of protocols (IP, ICMP, UDP, TCP etc), concurrency, packet loss, host failure, timeouts, the complex sockets interface to the protocols, and subtle portability issues. Moreover, the behavioural properties of operating systems and the network are not well documented.

A few of these issues have been addressed in the process calculus and distributed algorithm communities, but there remains a wide gulf between what has been captured in semantic models and what is required for a precise understanding of the behaviour of practical distributed programs that use these protocols.

In this paper we demonstrate (in a preliminary way) that the gulf can be bridged. We give an operational model for socket programming with a substantial fraction of UDP and ICMP, including loss and failure. The model has been validated by experiment against actual systems. It is not tied to a particular programming language, but can be used with any language equipped with an operational semantics for system calls -- here we give such a language binding for an OCaml fragment. We illustrate the model with a few small network programs.

[PS.GZ (156K)].


The UDP Calculus: Rigorous Semantics for Real Networking. Andrei Serjantov, Peter Sewell, and Keith Wansbrough (2001). Technical report. [Brief].

Abstract: Network programming is notoriously hard to understand: one has to deal with a variety of protocols (IP, ICMP, UDP, TCP etc), concurrency, packet loss, host failure, timeouts, the complex sockets interface to the protocols, and subtle portability issues. Moreover, the behavioural properties of operating systems and the network are not well documented.

A few of these issues have been addressed in the process calculus and distributed algorithm communities, but there remains a wide gulf between what has been captured in semantic models and what is required for a precise understanding of the behaviour of practical distributed programs that use these protocols.

In this paper we demonstrate (in a preliminary way) that the gulf can be bridged. We give an operational model for socket programming with a substantial fraction of UDP and ICMP, including loss and failure. The model has been validated by experiment against actual systems. It is not tied to a particular programming language, but can be used with any language equipped with an operational semantics for system calls -- here we give such a language binding for an OCaml fragment. We illustrate the model with a few small network programs.

University of Cambridge Computer Laboratory Technical Report [UCAM-CL-TR-515] [PS.GZ (277K)].


Simple Usage Polymorphism. Keith Wansbrough and Simon Peyton Jones (2000). In The Third ACM SIGPLAN Workshop on Types in Compilation, 21 September, 2000, Montreal, Canada. [Brief].

Abstract: We present a novel inference algorithm for a type system featuring subtyping and usage (annotation) polymorphism. This algorithm infers simply-polymorphic types rather than the constrained-polymorphic types usual in such a setting; it achieves this by means of constraint approximation. The algorithm is motivated by practical considerations and experience of a previous system, and has been implemented in a production compiler with positive results. We believe the algorithm may well have applications in settings other than usage-type inference.

[PS.GZ (132K)].


A Novel Problem in Constraint-Based Type Inference. Keith Wansbrough (1999). Unpublished note, November 22, 1999. [Brief].

Abstract: In previous work we have designed and implemented a system that automatically infers usage annotations for programs written in Core Haskell. Subsequently, however, we have found that the results of the inference are unacceptably poor, due to the usage-monomorphic nature of the analysis. Therefore, we are currently modifying the analysis to include usage polymorphism.

It appears that in the process we have uncovered a novel problem. Natural presentations of a system with subtyping and polymorphism involve bounded quantification, but our implementation experience leads us to judge this operator too expensive to implement in our testbed, the Glasgow Haskell Compiler. We therefore seek a way of getting by with only unbounded quantification.

Clearly in rejecting bounded quantification we lose some expressive power, and our analysis must be approximate. However, we have some evidence suggesting that in practice we should expect to find very little loss in precision. This loss should be weighed against a considerable gain in terms of smaller types, rapid inference, and ease of implementation.

In this note we present our (constraint- and bound-free) type system with subtyping and usage polymorphism, and discuss how one might go about inferring types for this system. The technical questions we hope to find answers for are: (i) What effective heuristics can be used to guide the approximation? and (ii) What is an appropriate theoretical framework in which to explore these issues?

[PS.GZ (113K)] .

Important clarifications and corrections to the above, January 20, 2000:
[PS.GZ (54K)].


Constraint-Based Type Inference with Subtyping and Recursive Types. Keith Wansbrough (1999). Talk given 8 November 1999 to Semantics Lunch, Computer Lab, University of Cambridge. [Brief].

[PS.GZ (slides only) (63K)].


Macros and Preprocessing in Haskell. Keith Wansbrough (1999). Unpublished. [Brief].

Abstract: Existing large Haskell systems make extensive use of the C preprocessor, CPP. Such use is problematic, as CPP is not designed for use with Haskell code. Certain features of the Haskell report also indicate a possible deficiency in the Haskell language. This paper investigates these deficiencies, and proposes two extensions to Haskell: the inclusion of distfix operators, and the incorporation of a Haskell preprocessor, HSPP, into the Haskell standard. Related issues are discussed, including the provision of a general macro facility for Haskell.

[PS.GZ (103K)].


Once Upon a Polymorphic Type. Keith Wansbrough and Simon Peyton Jones (1998). Technical Report TR-1998-19, Department of Computing Science, University of Glasgow.

This is the technical report version of the POPL'99 paper below. [Brief].

Abstract: We present a sound type-based `usage analysis' for a realistic lazy functional language. Accurate information on the usage of program subexpressions in a lazy functional language permits a compiler to perform a number of useful optimisations. However, existing analyses are either ad-hoc and approximate, or defined over restricted languages.

Our work extends the Once Upon A Type system of Turner, Mossin, and Wadler (FPCA'95). Firstly, we add type polymorphism, an essential feature of typed functional programming languages. Secondly, we include general Haskell-style user-defined algebraic data types. Thirdly, we explain and solve the `poisoning problem', which causes the earlier analysis to yield poor results. Interesting design choices turn up in each of these areas.

Our analysis is sound with respect to a Launchbury-style operational semantics, and it is straightforward to implement. Good results have been obtained from a prototype implementation, and we are currently integrating the system into the Glasgow Haskell Compiler.

[PS.GZ (214K)].


Once Upon a Polymorphic Type. Keith Wansbrough and Simon Peyton Jones (1999). Appears in The Twenty-sixth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 20-22, 1999, San Antonio, Texas.

See the technical report version above. [Brief].

Abstract: We present a sound type-based `usage analysis' for a realistic lazy functional language. Accurate information on the usage of program subexpressions in a lazy functional language permits a compiler to perform a number of useful optimisations. However, existing analyses are either ad-hoc and approximate, or defined over restricted languages.

Our work extends the Once Upon A Type system of Turner, Mossin, and Wadler (FPCA'95). Firstly, we add type polymorphism, an essential feature of typed functional programming languages. Secondly, we include general Haskell-style user-defined algebraic data types. Thirdly, we explain and solve the `poisoning problem', which causes the earlier analysis to yield poor results. Interesting design choices turn up in each of these areas.

Our analysis is sound with respect to a Launchbury-style operational semantics, and it is straightforward to implement. Good results have been obtained from a prototype implementation, and we are currently integrating the system into the Glasgow Haskell Compiler.

[PS.GZ (131K)] .

Slides of the talk:
[PS.GZ (POPL version) (71K)] [PS.GZ (full version) (96K)].


First Year Plan of Work: Usage Types for Compiler Optimisation. Keith Wansbrough (1998). Department of Computing Science, University of Glasgow, January 9, 1998. [Brief].

[PS.GZ (54K)] [DVI.GZ (9K)] [HTML (slightly mangled) (3K)].


Instance Declarations are Universal. Keith Wansbrough (1998). Unpublished note. [Brief].

Abstract: Following recent discussions about instance declarations in Haskell-2 on the Haskell mailing list, and the suggestion that without sufficient restrictions in this area Haskell's type system would become undecidable, I decided to demonstrate this directly. In this brief paper I present a construction that encodes a Turing machine directly in a series of instance declarations. The encoding is such that it forces the type checker to simulate the operation of a specified Turing machine in order to check the program. If the Turing machine terminates then the program is well-typed; if the Turing machine fails to terminate then it is ill-typed. The well-known undecidability of the Halting problem thereby carries across to the unrestricted version of the Haskell-2 type system.

[HTML (12K)].


A Modular Monadic Action Semantics. Keith Wansbrough and John Hamer (1997). In The Conference on Domain-Specific Languages, Proceedings, Santa Barbara, California, October 15-17, 1997, The USENIX Association, pp. 157-170. [Brief].

Abstract: A domain-specific language (DSL) is a framework which is designed to precisely meet the needs of a particular application. Domain-specific languages exist for a variety of reasons. As productivity tools, they are used to make application prototyping and development faster and more robust in the presence of evolving requirements. Furthermore, by bridging the ``semantic gap'' between an application domain and program code, DSLs increase the opportunity to apply formal methods in proving properties of an application.

In this paper, we contribute a synthesis of two existing systems that address the problem of providing sound semantic descriptions of realistic programming languages: action semantics and modular monadic semantics. The resulting synthesis, modular monadic action semantics, is compatible with action semantics yet adds true modularity and allows domain specific specifications to be made at a variety of levels.

[PS.GZ (66K)].


A Modular Monadic Action Semantics. Keith Wansbrough (1997). MSc thesis, Department of Computer Science, University of Auckland, February 1997. [Brief].

Abstract: Action semantics and modular monadic semantics are two independent approaches to the problem of specifying programming language semantics. Action semantics, developed by Mosses, is intended to be a system allowing ``useful semantic descriptions of realistic programming languages''; its worth has been demonstrated by the existence of action semantic descriptions of a number of relatively large languages. Modular monadic semantics is a more recent system developed by Espinosa and Liang, Hudak and Jones based on work done by Moggi; it is essentially an extension of concept of monads currently enjoying wide use for the represention of state in functional languages.

In this thesis we present modular monadic action semantics, a system that combines the best features of action semantics and modular monadic semantics. Modular monadic action semantics replaces the structural operational semantics that formalises action semantics with a modular monadic semantics. This replacement provides the flexibility to modify or delete existing facets of action semantics or to add entirely new ones, and will allow the use of the theories of modular monadic semantics and of denotational semantics to theorise about actions.

We have implemented modular monadic action semantics in the functional language Gofer, and in this thesis we discuss a number of issues that arose during the implementation relating to both action semantics and modular monadic semantics. The implementation clarified a number of facts relating to the structure of action semantics; it also contributed two new constructs to modular monadic semantics, representing I/O and parallelism. We demonstrate some of the power of modular monadic action semantics by adding a continuational facet to action semantics, allowing representation of the call/cc operation.

Available from my thesis page.


Tracing Lazy Functional Languages. Jeremy Gibbons and Keith Wansbrough (1996). In Proceedings of CATS: Computing - The Australasian Theory Seminar, Melbourne, January 1996, Michael E. Houle and Peter Eades, editors, pp. 11-20.

Also appears in Proceedings of the Third Massey Functional Programming Workshop, Palmerston North, New Zealand, 12-13 February 1996, Peter Burgess, editor; ISBN 0-473-03679-7. [Brief].

Abstract: We argue that Ariola and Felleisen's and Maraist, Odersky and Wadler's axiomatization of the call-by-need lambda calculus forms a suitable formal basis for tracing evaluation in lazy functional languages. In particular, it allows a one-dimensional textual representation of terms, rather than requiring a two-dimensional graphical representation using arrows. We describe a program LetTrace, implemented in Gofer and tracing lazy evaluation of a subset of Gofer.

[PS.GZ (53K)].


Tracing Lazy Functional Languages. Keith Wansbrough (October 11, 1995). BSc(Hons) project report. [Brief].

Abstract: The tracing of conventional imperative languages is straightforward, and tracing is probably the most common debugging technique in use today. However, attempting blindly to trace pure functional languages, especially lazy functional languages, does not work due to the fundamentally different model of execution. We claim that Ariola, Felleisen, Maraist, Odersky and Wadler's call-by-need lambda calculus provides a suitable formal model upon which to build a tracer for a lazy functional language, and we demonstrate this by exhibiting such a tracer, LetTrace. We also discuss a number of issues encountered in the implementation of this system, and propose a few areas for future work.

[PS.GZ (152K)].


A Methodology for Procedure Cloning. Keith Wansbrough (May, 1995). Assignment for paper 07.430, 1995, under Christian Collberg: paper summary/presentation. [Brief].

Abstract: Procedure cloning is an interprocedural optimisation technique that creates duplicates or `clones' of a procedure, each representing different sets of assumptions about the state on entry to the procedure. This opens the way for further optimisations of the procedure body.

This paper summarises another paper [Cooper 1993], presenting a three-phase algorithm for deciding which procedures in a program should be cloned, and how. The algorithm runs in polynomial time and bounds the code growth within reasonable limits.

[PS.GZ (27K)].


CC Programs with both In- and Non-determinism: A Concurrent Semantics; with an introduction to CCP. Keith Wansbrough (1995). Assignment for paper 07.460, 1995, under Hans Guesgen. Paper summary/presentation. [Brief].

Abstract: We present a summary of CC Programs with both In- and Non-determinism: A Concurrent Semantics [Montanari et. al. 1994], preceded by an introduction to the field of concurrent constraint programming (CCP), based largely on [Saraswat 1993].

[PS.GZ (34K)] [DVI (27K)].


A Natural Definition of Random Language. Keith Wansbrough (1995). Assignment for paper 07.455, 1995, under Cristian Calude. Project. [Brief].

Abstract: We propose a natural definition of random language, based on the standard AIT definitions of random string and random sequence. We demonstrate the equivalence of our natural definition with an existing, less natural definition.

[PS.GZ (36K)] [DVI (27K)].


Document publications/abstracts revised 22-Apr-2005.
Generated by PMT v1.1.