Rasmus Lerchedahl Petersen

Research Assistant at the department of Electronic Engineering and Computer Science, my field is computer science (PhD Scholarships available).

My research interests center around reasoning about programs. I pursue better tools for manual reasoning by investigating logic, type systems and semantics. I am also interested in better tools for automatic reasoning and recently built a thoerem prover for inductive definitions.

Basic information:

Title: Research Assistant
Ext: 5237
Room: CS/440
Phone: +44 (0) 207 882 5237
Email: rusmus@eecs.qmul.ac.uk
Research Group: Logic and Semantics

Research:

Refereed Journal Publications
- L. Birkedal, R.E. Møgelberg and R.L. Petersen:
- Category-theoretic models of Linear Abadi & Plotkin Logic
- Theory and Applications of Categories, Vol. 20, No. 7, 2008, pp. 116–151.
- online version
- L. Birkedal, R.E. Møgelberg and R.L. Petersen:
- Domain-theoretic models of parametric polymorphism
- Theoretical Computer Science Volume 388, Issues 1-3, 5 December 2007, Pages 152-172
- online version
- L. Birkedal, R.E. Møgelberg and R.L. Petersen:
- Linear Abadi and Plotkin logic
- Logical Methods in Computer Science, 2(5:2), August 2006
- online version
Refereed Conference Publications
- R. Grigore, R.L. Petersen and D. Distefano:
- TOPL: A Language for Specifying Safety Temporal Properties of Object-Oriented Programs
- To appear at FOOL 2011
- .pdf
- C.A.R. Hoare, A. Hussain, B. Möller, P.W. O’Hearn, R.L. Petersen and G. Struth:
- On Locality and the Exchange Law for Concurrent Processes
- CONCUR 2011
- .pdf
- J. Brotherston, D. Distefano and R.L. Petersen:
- Automated Cyclic Entailment Proofs in Separation Logic
- CADE 2011
- .pdf
- O. Lee, H. Yang and R.L. Petersen:
- Program analysis for overlaid data structures
- CAV 2011
- .pdf
- R.L. Petersen, L. Birkedal, A. Nanevski and G. Morrisett:
- A Realizability Model for Impredicative Hoare Type Theory
- ESOP 2008
- online version
- L. Birkedal, R.E. Møgelberg and R.L. Petersen:
- Parametric Domain-theoretic models of polymorphic intuitionistic / linear lambda calculus
- Mathematical Foundations of Programming Semantics XXI, 25 pages. Feb 2005
- .ps or .pdf
Technical Reports
- L. Birkedal, R.E. Møgelberg and R.L. Petersen:
- Parametric Domain-theoretic models of Linear Abadi & Plotkin Logic
- Technical Report TR-2005-57, IT University of Copenhagen, 76 pages. Feb 2005
- .ps or .pdf
- R.E. Møgelberg, L. Birkedal and R.L. Petersen:
- Categorical models of PILL
- Technical ReportTR-2005-58, IT University of Copenhagen, 17 pages. Feb 2005
- .ps or .pdf
My Ph.D. dissertation
- R.L. Petersen:
- Abstractions with Reasoning Principles via Denotational Semantics
- Ph.D. Dissertation, 192 pages. Aug 2007
- .pdf
My masters thesis
- R.L. Petersen:
- A Concrete Parametric Domain-theoretic Model of PILLY
- Masters Thesis, 81 pages. Aug 2005
- .pdf
- R.L. Petersen:
- Slides from my defence
- .pdf
PR:
- R.L. Petersen:
- On Locality and the Exchange Law for Concurrent Processes
- Slides from my presentation at CONCUR 2011
- .pdf
- R.L. Petersen:
- Automated Cyclic Entailment Proofs in Separation Logic
- Slides from my presentation at CADE 2011
- .pdf
- L. Birkedal, R.E. Møgelberg, R.L. Petersen:
- Parametricity Poster
- We put together this poster to explain the concept of parametricity
- .pdf
- R.L. Petersen:
- LILY Lunch Talk
- I assembled these slides to present the LILY language at the weekly lunch talk in the PLS Group
- .pdf