My papers and publications, in reverse order of publication. A list including 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. [Abstract] [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. [Abstract] 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. [Abstract] 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. [Abstract] [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. [Abstract] [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. [Abstract] 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. [Abstract] [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. [Abstract] [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. [Abstract] 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. [Abstract] [PS.GZ (767K)].
Global Abstraction-Safe Marshalling with Hash Types. James J. Leifer, Gilles Peskine, Peter Sewell, Keith Wansbrough (2004). Technical report. [Abstract] 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. [Abstract] [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. [Abstract] 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. [Abstract] 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. [Abstract] [PS.GZ (156K)].
The UDP Calculus: Rigorous Semantics for Real Networking. Andrei Serjantov, Peter Sewell, and Keith Wansbrough (2001). Technical report. [Abstract] 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. [Abstract] [PS.GZ (132K)].
A Novel Problem in Constraint-Based Type Inference. Keith Wansbrough (1999). Unpublished note, November 22, 1999. [Abstract] [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. [Abstract] [PS.GZ (slides only) (63K)].
Macros and Preprocessing in Haskell. Keith Wansbrough (1999). Unpublished. [Abstract] [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. [Abstract] [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. [Abstract] [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. [Abstract] [PS.GZ (54K)] [DVI.GZ (9K)] [HTML (slightly mangled) (3K)].
Instance Declarations are Universal. Keith Wansbrough (1998). Unpublished note. [Abstract] [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. [Abstract] [PS.GZ (66K)].
A Modular Monadic Action Semantics. Keith Wansbrough (1997). MSc thesis, Department of Computer Science, University of Auckland, February 1997. [Abstract] 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. [Abstract] [PS.GZ (53K)].
Tracing Lazy Functional Languages. Keith Wansbrough (October 11, 1995). BSc(Hons) project report. [Abstract] [PS.GZ (152K)].
A Methodology for Procedure Cloning. Keith Wansbrough (May, 1995). Assignment for paper 07.430, 1995, under Christian Collberg: paper summary/presentation. [Abstract] [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. [Abstract] [PS.GZ (34K)] [DVI (27K)].
A Natural Definition of Random Language. Keith Wansbrough (1995). Assignment for paper 07.455, 1995, under Cristian Calude. Project. [Abstract] [PS.GZ (36K)] [DVI (27K)].