gmb://publications

From Java to UpgradeJ: An empirical study. (with Tempero, Parkinson and Noble) Submitted. July 2008.

UpgradeJ: Incremental typechecking for class upgrades. (with Parkinson and Noble) Proceedings of 22nd ECOOP. LNCS 5142. Pages 235-259. July 2008. pdf

Dynamic Rebinding for Marshalling and Update, via Redex-time and Destruct-time Reduction. (with Hicks, Sewell, Stoyle and Wansborough) Journal of Functional Programming, Volume 18, issue 04, pages 437-502. July 2008.

Selected papers from the 10th International Symposium on Database Programming Languages (DBPL 2005). (co-edited with Koch). Information Systems, Volume 33, Issue 4-5 (Special edition). June 2008.

UpgradeJ: Incremental typechecking for class upgrades (long version). (with Parkinson and Noble) University of Cambridge Computer Laboratory Technical Report 716. April 2008. 33+iipp. pdf

Separation logic, abstraction and inheritance. (with Parkinson) Proceedings of 35th POPL. Pages 75-86. January 2008. pdf

Lost in translation: Formalizing proposed extensions to C# (with Meijer and Torgersen) Proceedings of 22nd OOPSLA. October 2007. [pdf corrected version (12 Nov 07)]

Mutatis Mutandis: Safe and predictable dynamic software updating (Journal Version). (with Stoyle, Hicks, Sewell and Neamtiu) ACM Transactions on Programming Languages and Systems. Volume 29, issue 4, article 22. August 2007. 70pp. pdf (Requires ACM account)

Formalizing and extending C# type inference. International Workshop on Foundations and Developments of Object-Oriented Languages (FOOL/WOOD '07). January 2007. [There's a slip in the on-line paper - I'll update soon.]

LINQ: Reconciling objects, relations and XML in the .NET framework. (with Meijer and Beckman) Proceedings of ACM SIGMOD 2006. pdf (One page abstract - full version to appear) Page 706. June 2006.

Report on 10th International Symposium on Database Programming Languages (DBPL 2005). (with Koch). SIGMOD Record, 35(1). March 2006. 6pp pdf

Proceedings of 10th International Symposium on Database Programming Languages (DBPL 2005). (edited with Koch) Volume 3774 of Springer LNCS. (Contents available online via springerlink.)

First-class relationships in an object-oriented language (Extended version). (with Wren) University of Cambridge Computer Laboratory Technical Report 642. August 2005. 53pp. pdf

The essence of data access in Cω. (with Meijer and Schulte) Proceedings of 19th ECOOP. LNCS 3586. Pages 287-311. July 2005. pdf © Springer-Verlag

First-class relationships in an object-oriented language. (with Wren) Proceedings of 19th ECOOP. LNCS 3586. Pages 262-286. July 2005. pdf © Springer-Verlag

Unifying tables, objects and documents. (with Meijer and Schulte). Proceedings of DP-COOL. Volume 27 of John von Neumann Institute of Computing. pdf

First-class relationships in an object-oriented language. (with Wren) Paper appeared in informal proceedings of 12th FOOL. January 2005. pdf

Mutatis Mutandis: Safe and predictable dynamic software updating. (with Stoyle, Hicks, Sewell and Neamtiu) Proceedings of 32nd POPL. Pages 183-194. January 2005. pdf © ACM.

Separation logic and abstraction. (with Parkinson) Proceedings of 32nd POPL. Pages 247-258. January 2005. pdf © ACM.

Dynamic rebinding for marshalling and update, with destruct-time lambda. (with Hicks, Sewell, Stoyle and Wansborough) University of Cambridge Computer Laboratory Technical Report 568. February 2004. 83+ii pp. pdf

Programming with circles, triangles and rectangles. (with Meijer and Schulte) Proceedings of XML 2003. html [IE-only version] and html [all browsers]. (My first paper written in XML!)

Ubiquitous Data. (with Buneman and Gardner) Position paper presented at UK-UbiNet Workshop 2003. September 2003. pdf

Dynamic rebinding for marshalling and update, with destruct-time lambda. (with Hicks, Sewell, Stoyle and Wansborough) Proceedings of ACM ICFP 2003. Pages 99-110. August 2003. pdf

Formal semantics and analysis of object queries (Extended Abstract). Proceedings of ACM SIGMOD 2003. Pages 407-418. June 2003. pdf

MJ: An imperative core calculus for Java and Java with effects. (with Parkinson and Pitts) University of Cambridge Computer Laboratory Technical Report 563. April 2003. 51+ii pp. pdf

Effects and effect inference for a core Java calculus. (with Parkinson) Proceedings of Workshop on Object-Oriented Developments (WOOD'03). ENTCS 82(8). April 2003. pdf

Formalizing dynamic software updating (Extended Abstract). (with Hicks, Sewell and Stoyle) Proceedings of Workshop on Unexpected Software Evolution (USE'03). April 2003. pdf

Iota: A concurrent, XML scripting language with applications to Home-Area Networks. (with Sewell) University of Cambridge Computer Laboratory Technical Report 557. January 2003. pdf

Inferring the principal type and schema requirements of an OQL query. (with Trigoni) Proceedings of 18th British National Conference on Databases. In Volume 2097 of Lecture Notes in Computer Science. Ed: B.J. Read. Pages 185-201. July 2001. © Springer-Verlag. pdf

Strong normalisation of cut-elimination in classical logic. (with Urban) Fundamenta Informaticae. 45(1-2):123-155. January 2001. pdf

On an Intuitionistic Modal Logic. (with de Paiva) Studia Logica. 65(3):383-416. 2000.

Operational properties of Lily, a polymorphic linear lambda calculus with recursion. (with Pitts and Russo) Proceedings of Fourth International Workshop on Higher Order Operational Techniques in Semantics (HOOTS). Volume 41 of Electronic Notes in Theoretical Computer Science, Elsevier. September 2000. 19pp. pdf

Towards a formal type system for ODMG OQL. (with Trigoni) University of Cambridge Computer Laboratory Technical Report 497. September 2000. 20pp. pdf

Using XML as an object interchange format. Proposal submitted to ODMG. Available on the ODMG website. pdf [local]

Program equivalence in a linear functional language. Journal of Functional Programming. 10(2):167-190. 2000. pdf © Cambridge University Press

A classical linear lambda calculus. Theoretical Computer Science. 227(1-2):43-78. 1999.

Strong normalisation of cut elimination in classical logic. (with Urban) Proceedings of the Fourth International Conference on Typed Lambda Calculus and Applications. In Volume 1581 of Lecture Notes in Computer Science, Springer Verlag. L'Aquila, Italy. April 1999. pdf

Multiple modalities. University of Cambridge Computer Laboratory Technical Report 455. December 1998. 26+ii pp. pdf

A computational interpretation of the -calculus. University of Cambridge Computer Laboratory Technical Report 448. September 1998. 27+ii pp. pdf (A more complete, albeit unpublished, version can be found here (pdf).)

A computational interpretation of the -calculus. Proceedings of Symposium on Mathematical Foundations of Computer Science. In Volume 1450 of Lecture Notes in Computer Science. Brno, Czech Republic. Eds: L. Brim, J. Gruska and J. Zlatuska. Pages 336-345. August 1998. © Springer-Verlag. pdf

Linear logic. In Routledge Encyclopedia of Philosophy. 2200 words. Published July 1998.

Computational types from a logical perspective. (with Benton and de Paiva). Journal of Functional Programming, 8(2):177-193. March 1998

A new general purpose parallel database system. (with Afshar, Bates and Moody). Abridged paper appears in Proceedings of IEEE International Symposium on Parallel Architectures, Algorithms and Networks. Pages 2-8. December 1997. pdf

Observations on a linear PCF. University of Cambridge Computer Laboratory Technical Report 412. January 1997. 30pp. pdf

Towards a classical linear lambda-calculus. Proceedings of Tokyo Meeting on Linear Logic. Volume 3 of Electronic Notes in Theoretical Computer Science , Elsevier. Eds J.-Y. Girard, M. Okada and A. Scedrov. November 1996. 13pp. pdf

A note on full intuitionistic linear logic. Annals of Pure and Applied Logic, 79(3):281-287. 1996.

A classical linear lambda-calculus. University of Cambridge Computer Laboratory Technical Report 401. July 1996. 41pp. (Superseded by journal version.) pdf

Intuitionistic necessity revisited. (with de Paiva). Technical Report CSRP-96-10, School of Computer Science, University of Birmingham. June 1996. 18pp. pdf (Superseded by journal version)

Computational types from a logical perspective I. (with Benton and de Paiva). University of Cambridge Computer Laboratory Technical Report 365. May 1995.

What is a categorical model of intuitionistic linear logic? Proceedings of the Second International Conference on Typed Lambda Calculus and Applications. In Volume 902 of Lecture Notes in Computer Science, Springer Verlag. Edinburgh, Scotland, April 1995. Pages 73-93. Previously available as Laboratory Technical Report 333, March 1994. © Springer-Verlag. pdf

On intuitionistic linear logic. PhD Thesis, University of Cambridge Computer Laboratory, December 1993. Available as Technical Report 346, August 1994. pdf

A term calculus for intuitionistic linear logic. (with Benton, de Paiva and Hyland). Proceedings of the First International Conference on Typed Lambda Calculus and Applications. In Volume 664 of Lecture Notes in Computer Science, Springer Verlag. 1993. Pages 75-90. © Springer-Verlag . pdf

Linear lambda-calculus and categorical models revisited. (with Benton, de Paiva and Hyland). Proceedings of Sixth Conference on Computer Science Logic. In Volume 702 of Lecture Notes in Computer Science, Springer Verlag. 1993. Pages 61-84. © Springer-Verlag. pdf

Intuitionistic necessity revisited (extended abstract). (with de Paiva). In Proceedings of Applied Logic Conference, December 1992.

Term assignment for intuitionistic linear logic. (with Benton, de Paiva and Hyland). Technical Report 262, University of Cambridge Computer Laboratory. August 1992. pdf