Matthew Parkinson

Research

I am now a Royal Academy of Engineering and EPSRC Research Fellow in the Computer Lab. I previously worked at Middlesex University with Professor Richard Bornat on Separation logic and concurrency. Before that I was a Ph.D. student in the Theory and Semantics group supervised by Dr Gavin Bierman and Professor Andrew Pitts. In October 2005 I successfully defended my Thesis on "Local Reasoning in Java". My thesis extended separation logic to a Java like setting, and was a runner-up in the BCS distinguished dissertation competition.

I previously organised the Theory Mini-courses. These are now organised by Sam Staton

Upcoming events

• VAMP'09: Verification and Analysis of Multi-threaded Java-like Programs [PC Member]

Publications

Separation Logic for Java

• jStar: Towards Practical Verification for Java (with Distefano) to appear in proceedings of OOPSLA'08
• Separation logic, abstraction and inheritance (with Bierman) in proceedings of POPL'08
• Class Invariants: the end of the Road presented at IWACO 2007.
• When separation logic met Java. in Proceedings of FTfJP 2006.
• Local Reasoning for Java, Ph.D. Thesis, Submitted Aug 2005. Final Version; and a Technical Report (Identical content, but more compactly typeset.) The thesis was a runner-up in the BCS distinguished dissertation competition.
• Separation logic and abstraction, (with Bierman) Proceedings of 32nd POPL. Pages 247-258. Jan 2005

Separation Logic for Concurrency

• Modular Safety Checking for Fine-Grained Concurrency (with Calcagno and Vafeiadis) in proceedings of SAS 2007.
• A marriage of Rely/Guarantee and Separation Logic (with Vafeiadis) in proceedings of CONCUR 2007. [Slides] [Old Version (Nov 1, 2006)]
• Modular Verification of a Non-Blocking Stack (with Bornat and O'Hearn) in Proceedings of POPL 2007. (This paper supersedes an earlier draft title "Exploiting linearizability in Separation logic".)
• Variables as resource in Hoare logic. (with Bornat and Calcagno) in Proceedings of LICS, 2006.
• Permission Accounting in Separation Logic, (with Bornat, Calcagno, and O'Hearn.) Proceedings of 32nd POPL. Pages 259-270. Jan 2005

Java Semantics

• UpgradeJ: Incremental Typechecking for Class Upgrades (DRAFT) (with Bierman and Noble).
• The Java Module System: core design and semantic definition (with Strnisa and Sewell) Proceedings of OOPSLA 2007.
• Effects and effect inference for a core Java calculus. (with Bierman) Proceedings of Workshop on Object-Oriented Developments (WOOD'03). ENTCS 82(8). April 2003. (The slides from WOOD'03.)
• MJ: an imperative core calculus for Java and Java with effects (with Bierman and Pitts) University of Cambridge Computer Laboratory Technical report 563. April 2003.

Talks

• Minicourse on Separation Logic: I presented a short course (two hours) introducing some of the ideas in separation logic: Part I and Part II.
• Proofs about concurrent programs. A high-level overview of the work on combining Rely-guarantee and separation logic. This is an informal, and short, introduction to the motivation and reasoning underly A marriage of Rely/Guarantee and Separation Logic and Modular Safety Checking for Fine-Grained Concurrency.

Ph.D. Students and Postdocs

Post-docs

• Mike Dodds Combining ideas from rely/guarantee and separation logic.

Students

I am primary supervisor to

• John Wickerson
• Eric Koskinen (Jointly supervised with Byron Cook)

I am second supervisor to

• Rok Strniša
• Magnus Myreen
• Thomas Türk
• Jonathan Mak

I was a joint supervisor to

• Viktor Vafeiadis [Defend 2007]

Teaching

Lecturing

I am the lecturer for Foundations of Functional Programming for 2008 and 2009.

Supervisions

I have supervised the following courses for Churchill College.
In Part IB: Logic and Proof, Semantics, Foundations of Functional Programming and Prolog.
In Part II: Types, Specification and Verification I and Topics in Concurrency.

Contact Details

EMail:	Matthew.Parkinson at cl.cam.ac.uk
Address:	University of Cambridge Computer Laboratory William Gates Building JJ Thomson Avenue Cambridge CB3 0FD, UK

Miscellaneous

I would like to thank Gareth Stoyle for letting me steal, and modify, his CSS.

Some random links: one to my friend Ewan Mellor's webpage to boost his page rank. He did his final year project on Iota with Gavin Bierman, and also has some great lisp for Sawfish. And a second to Chris Morgan's website as he also wants more pagerank! Finally, a link to alpha-plus where Lisa works.

Here are some companies I have worked for:

• Leaguevision Limited a web design, draughting, and CAD company based in Nottingham.
• Invest Solutions Limited a software and hardware consultancy based in Cambridge.