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
News
-
Funding for post-doc job in verifying concurrent programs (see advert).
-
Funding for Ph.D. student in verifying concurrent programs. (Details to appear.)
-
Separation logic, abstraction and inheritance (with Bierman) accepted to appear at POPL'08
Ph.D. Students
I am second supervisor to
Publications
Separation Logic
-
Separation logic, abstraction and inheritance (with Bierman) accepted to appear at POPL'08
-
Class Invariants: the end of the Road presented at IWACO 2007.
-
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".)
-
When separation logic met Java. in Proceedings of FTfJP 2006.
-
Variables as resource in Hoare logic. (with Bornat and Calcagno) in Proceedings of LICS, 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.
-
Permission Accounting in Separation
Logic, (with Bornat, Calcagno, and O'Hearn.) Proceedings of 32nd POPL. Pages 259-270. Jan 2005
-
Separation logic and abstraction,
(with Bierman) Proceedings of 32nd POPL. Pages 247-258. Jan 2005
I have also presented a short abstract at
AppSem04 on
When separation logic met Java.
Java Semantics
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.
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!
Here are some companies I have worked for: