- Deciding equivalence using type checking Workshop: abstraction and verification in semantics, June 2014

- An introduction to deciding higher-order matching Invited talk at GALOP, July 2013

- Proof systems for retracts in simply typed lambda calculus ICALP, July 2013

- Applying automata and games to simply typed lambda calculus Invited talk at EXPRESS/SOS, September 2012

- An introduction to deciding higher-order matching Invited talk at British Logic Colloquium, September 2010

- Dependency tree automata Fossacs 2009 talk, March 2009

- lecture one lecture two lecture three lecture four Marktoberdorf Summerschool 2005

- lecture one lecture two lecture three lecture four International Winter School, Montevideo, Uruguay, 2003

- Edited Plotkin, Stirling, Tofte
*Proof, Language, and Interaction Essays in Honour of Robin Milner*

MIT Press, 2000 *Modal and Temporal Properties of Processes*

Springer (Texts in Computer Science), 2001

- Proof systems for retracts in simply typed
lambda calculus

ICALP 2013.

Full version of abstract in*Lecture Notes in Computer Science*7966, 404-415, 2013. - An introduction to decidability of
higher-order matching

Submitted for publication. Latest version July 2013. - Bisimulation and logic

In*Advanced topics in Bisimulation and Coinduction*ed. D. Sangiorgi and J. Rutten, 173-196, Cambridge University Press, 2011. - Decidability of higher-order matching

In*Logical Methods in Computer Science*5, 1-52, 2009 (special issue for ICALP 06). - Dependency tree automata

FOSSACS 2009*Lecture Notes in Computer Science*5504, 92-106, 2009. - Higher-order matching, games and automata

LICS 2007 (Invited talk), 326-335 - Model-checking games for typed lambda-calculi

In*Electronic Notes in Theoretical Computer Science (ENTCS)*172, 589-610, 2007 - With J. Bradfield

Modal mu-calculi (ps version)

In*Handbook of Modal Logic*editors P. Blackburn, J. van Benthem and F. Wolter*Studies in Logic and Practical Reasoning Volume 3*, Elsevier, 721-756, 2007

See Handbook web site - Second-order simple grammars
(ps version)

CONCUR 2006*Lecture Notes in Computer Science*4137, 509-523, 2006 - A game-theoretic approach to deciding
higher-order matching
(pdf)

ICALP 2006*Lecture Notes in Computer Science*4052, 348-359, 2006 - Language theory and infinite graphs
(pdf)

Notes for*Logical aspects of secure computer systems*

Marktoberdorf summerschool 2005 (Shortened final version pdf) - Higher-order matching and games
(pdf)

CSL 2005*Lecture Notes in Computer Science*3634, 119-134, 2005 - Bisimulation and language equivalence
(pdf)

In*Logic for Concurrency and Synchronisation*edited Ruy de Quieroz,*Trends in Logic*Vol. 18, Kluwer, 269-284, 2003 - Deciding DPDA equivalence is primitive recursive
(pdf)

ICALP 2002*Lecture Notes in Computer Science*2380, 821-832, 2002

(Longer draft paper pdf) - With M. Lange

Model checking fixed point logic with chop (pdf)

FOSSACS 2002*Lecture Notes in Computer Science*2303, 250-263, 2002 - With M. Lange

Model checking games for branching time logics (pdf)*Journal of Logic and Computation*12, 623-639, 2002 - An introduction to decidability of DPDA equivalence
(pdf)

FSTTCS 2001 (invited talk)*Lecture Notes in Computer Science*2245, 42-56, 2001 - Decidability of DPDA equivalence
(pdf)
*Theoretical Computer Science*255, 1-31, 2001 - With C. Morvan

Rational graphs trace context-sensitive languages (pdf)

MFCS 2001*Lecture Notes in Computer Science*2136, 548-559, 2001 - With M. Lange

Focus games for satisfiability and completeness of temporal logic (pdf)

LICS 2001, 357-365 - Decidability of weak bisimilarity for a subset of
basic parallel processes (pdf)

FOSSACS 2001*Lecture Notes in Computer Science*2030, 379-393, 2001 - With J. Bradfield

Modal logics and mu-calculi

In*Handbook of Process Algebra*, edited J. Bergstra, A. Ponse and S. Smolka, 293-332

Elsevier, North-Holland, 2001 - Schema revisited (pdf)

CSL 2000 (invited talk)*Lecture Notes in Computer Science,*1862, 126-138, 2000 - Decidability of bisimulation equivalence
for pushdown processes (pdf)

Draft Paper, 2000 - With T. Kempster and P. Thanisch

Diluting ACID*ACM SIGMOD RECORD 28(4)*, 1999 - Bisimulation, modal logic and model checking games
*Logic Journal of the IGPL*7, 103-124, 1999 - The joys of bisimulation
(pdf)

MFCS 1998 (invited talk)*Lecture Notes in Computer Science*1450, 142-151, 1998 - Decidability of bisimulation equivalence for
normed pushdown processes
*Theoretical Computer Science*195, 113-131, 1998 - With T. Kempster and P. Thanisch

A more committed quorum-based three phase commit protocol

DISC 1998*Lecture Notes in Computer Science*1499, 246-257, 1998 - With P. Stevens

Practical model-checking using games

TACAS 1998*Lecture Notes in Computer Science*, 1384, 85-101, 1998 - With H. Huttel

Actions speak louder than words: proving bisimilarity for context-free processes (pdf)*Journal of Logic and Computation*8(4), 485-509, 1998 - Bisimulation, model checking and other games
(pdf)
*Notes for Mathfit instructional meeting on games and computation*, Edinburgh, June 1997 - Decidability of bisimulation equivalence for
normed pushdown processes

CONCUR 1996*Lecture Notes in Computer Science*1119, 217-232, 1996 - Games for bisimulation and model checking
*Notes for Mathfit Workshop on finite model theory*, University of Wales, Swansea, July 1996 - Games
and modal mu-calculus (pdf)

TACAS 1996*Lecture Notes in Computer Science*1055, 298-312, 1996 -
Modal and temporal logics for processes
(pdf)
*Lecture Notes in Computer Science*1043, 149-237, 1996 - Local model checking games
(pdf)

CONCUR 1995 (invited talk)*Lecture Notes in Computer Science*962, 1-11, 1995 - With S. Christensen and H. Huttel

Bismulation equivalence is decidable for all context-free processes (pdf)*Information and Computation*121, 143-148, 1995 (Extended version from Concur92) - With H. Andersen and G. Winskel

A compositional proof system for model checking (pdf)

This is an extended version of a LICS 1994 paper, 144-153 (The lics version pdf)