I work as a research and teaching assistant at the Department of Theoretical Computer Science of the LMU Munich.

Past activities:

- Feb–Aug 2009 Fellow, Institute of Advanced Studies, University of Bologna
- 2005–2008 Research assistant on the DFG project Pro.Platz, LMU Munich
- 2001–2005 PhD at LFCS, Edinburgh, supervised by Ian Stark
- 2000–2001 MSc at LFCS, Edinburgh, supervised by Alex Simpson
- 1996–2000 Informatics studies at the University of Leipzig

### Publications, Slides, Drafts

- Functional Programming in Sublinear Space
- With Ugo Dal Lago.
- Last revision: 18 March 2010; this version corrects a few typos; the original publication is available at www.springerlink.com.
- In
*European Symposium on Programming (ESOP2010)*, Cyprus, 2010, ©Springer-Verlag,*to appear* *Slides:*OASIS Seminar, Oxford University (December 2009)

- Pointer Programs and Undirected Reachability
- With Martin Hofmann.
- In
*Logic in Computer Science (LICS09)*, Los Angeles, USA - to appear, ©IEEE
*Slides:*LICS09 (August 2009)

- Pointer Programs and Undirected Reachability (long version)
- With Martin Hofmann.
*Electronic Colloquium on Computational Complexity (ECCC)*- ECCC Technical Report TR08-090
- (last revision: January 16, 2009)

- Pure Pointer Programs with Iteration (long version)
- With Martin Hofmann.
- In
*Transactions of Computational Logic (ToCL)*, 2009,*to appear*

- A Formalised Lower Bound on Undirected Graph Reachability
- (Coq sources)
- Revised version to appear in
*LPAR 2008*

- Pure Pointer Programs with Iteration
- With Martin Hofmann.
- In
*Computer Science Logic (CSL08)*, Bertinoro, Italy - LNCS 5213, 2008, ©Springer-Verlag

- Stratified Bounded Affine Logic for Logarithmic Space
- In
*Logic in Computer Science (LICS07)*, Wroclaw, Poland, ©IEEE - Draft full version, comments welcome!
*Slides:*LICS07 (July 2007)

- Space-efficient Computation by Interaction – A Type System for Logarithmic Space
- In
*Computer Science Logic (CSL06)*, Szeged, Hungary - LNCS 4207, 2006, ©Springer-Verlag
*Slides:*CSL06 (September 2006)

- Modelling Generic Judgements
- In
*International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP06)*, Seattle, USA, 2006, Appears in ENTCS 174(5), 2007 *Slides:*LFMTP06 (August 2006)

- Names and Binding in Type Theory
- PhD Thesis, The University of Edinburgh, 2006
*Slides:*ICMS07 (May 2007)

- A Dependent Type Theory with Names and Binding
- With Ian Stark.
- In
*Computer Science Logic (CSL04)*, Karpacz, Poland - LNCS, 3210, pages 235–249, 2004
*Slides:*CSL04 (September 2004), Logic and Semantics Club at LFCS (August 2004)

- Verifying Temporal Properties using Explicit Approximants: Completeness for Context-free Processes. (Older version with outline proofs)
- With Alex Simpson.
- In
*Proceedings of Foundations of Software Science and Computation Structures (FOSSACS02)*, Grenoble, France - LNCS, 2303, pages 372–386, 2002, ©Springer-Verlag
*Slides:*FoSSaCS02 (April 2002), Logic and Semantics Club at LFCS (February 2002)

- Formal Verification of Processes
- MSc thesis, The University of Edinburgh, 2001