Share this page
  • Share this page on Twitter Share this page on Facebook Share this page on Digg Share this page on Del.icio.us Read the Inside Microsoft Research blog
  • E-mail this page Print this page
  • RSS feeds
Home > People > Gavin Bierman
Gavin Bierman

Gavin Bierman is a senior researcher in the Programming Principles and Tools Group at Microsoft Research in Cambridge, UK. His areas of interest include database query languages, big data, type systems, semantics, programming language design and implementation, separation logic, and dynamic software updating.  

Publications

  • Pause 'n' play: Formalizing asynchronous C#. (with Russo, Mainland, Meijer and Torgersen). Proceedings of ECOOP 2012. LNCS 7313. Pages 233-257. June 2012. © Springer-Verlag.
  • Extending the relational algebra with similarities. (with Hajdinjak). Mathematical Structures in Computer Science. 2012. © Cambridge University Press [PDF]
  • Semantic subtyping with an SMT solver. (with Gordon, Hritcu and Langworthy). Journal of Functional Programming, 22(1):31-105. March 2012. © Cambridge University Press [PDF]
  • A co-relational model of data for large shared data banks. (with Meijer). Communications of ACM Volume 54, number 4, pp49-58, and ACM Queue, Volume 9, Number 3. March 2011. [web]
  • Semantic subtyping with an SMT solver. (with Gordon, Hritcu and Langworthy). Microsoft Research Technical Report MSR-TR-2010-99. December 2010.
  • Semantic subtyping with an SMT solver. (with Gordon, Hritcu and Langworthy). Proceedings of ICFP 2010. September 2010. © ACM [PDF]
  • Adding dynamic types to C#. (with Meijer and Torgersen). Proceedings of ECOOP 2010. June 2010. © Springer Verlag [PDF - important corrected version, errata]
  • UpgradeJ: Incremental typechecking for dynamic class upgrades. (with Parkinson and Noble). Submitted to journal. 2009
  • A theory of typed coercions and its applications. (with Hicks and Swamy) Proceedings of ICFP. August 2009 [PDF] © ACM
  • From Java to UpgradeJ: An empirical study. (with Tempero, Parkinson and Noble) Proceedings of 1st Workshop on Hot Topics in Software Upgrades. October 2008 [PDF]
  • UpgradeJ: Incremental typechecking for class upgrades. (with Parkinson and Noble) Proceedings of 22nd ECOOP. LNCS 5142. Pages 235-259. July 2008. © Springer-Verlag [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. © Springer-Verlag [PDF]
  • First-class relationships in an object-oriented language. (with Wren) Proceedings of 19th ECOOP. LNCS 3586. Pages 262-286. July 2005. © Springer-Verlag [PDF]
  • 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 lambda-mu-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 lambda-mu-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 , lsevier. 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]

Talks

  • Adding dynamic types to C#. ECOOP'10. June 23, 2010. [pdf]
  • UpgradeJ: Incremental typechecking for class upgrades. ECOOP'08. July 10, 2008. [pdf]
  • Lost in translation: Formalizing proposed extensions to C#. OOPSLA'07. October 25, 2007. [pdf]
  • The essence of data access in Cw. ECOOP'05. July 28, 2005. [pdf]

Community

ECOOP 2012 [PC member]; DBPL 2011 [PC member]; FTfJP 2011 [PC member]; ECOOP 2011 [PC member]; STOP 2011 [PC member]; MPOOL 2010 [PC member]; RAOOL 2009 [PC member]; DBPL 2009 [PC member]; HotSWUp 2009 [PC member]; PLAN-X 2009 [co-chair]; ECOOP 2008 [PC member]; HotSWUp 2008 [PC member]; IMLA 2008 [PC member]; RAOOL 2008 [PC member]; PLAN-X 2006 [PC member]; FOOL/WOOD 2006 [PC member]; DBPL 2005 [co-chair]; MPOOL 2005 [PC member]; APPSEM 2004 [PC member]

Brief Bio

Gavin Bierman is currently a senior researcher in the Programming Principles and Tools Group, headed by Luca Cardelli, at Microsoft Research in Cambridge, UK. He joined MSR in March 2004; previously (Oct 2000-Mar 2004) he was a University Lecturer at the University of Cambridge Computer Laboratory and a Fellow, College Lecturer & Director of Studies at St. Johns College, Cambridge.

He is proud to have supervised the following research students:

He also taught the following courses:  Database Theory [Lent Term, 2004]; Introduction to Functional Programming [Lent Term 2004]; Databases [Easter Term 2004]; Databases [Easter Term 2003]; Database Theory [Easter Term 2003]; Databases [Easter Term 2002]; Operating Systems Foundations [Mich Term 2001]; Introduction to Functional Programming [Lent Term 1999].

Prior to this he was a University Lecturer at the University of Warwick Department of Computer Science (Sept 1999-Sept 2000), a Research Fellow at Gonville and Caius College, Cambridge (Oct 1995-Sep 1999), an EPSRC research associate (Oct 1995-Sept 1997), and a non-stipendiary Research Fellow at Wolfson College, Cambridge (Oct 1993-Sept 1995). His PhD is from the University of Cambridge Computer Laboratory (Oct 1990-Dec 1993), and his BSc(Eng) from Imperial College.

Contact details

Microsoft Research
Roger Needham Building
7 JJ Thomson Avenue
Cambridge CB3 0FB
UK
Email: gmb at microsoft dot com
Phone: +44 1223 479 788
Fax: +44 1223 479 999
http://research.microsoft.com/users/gmb
How to get to MSR Cambridge