Colin Stirling

Research Interests

Models and calculi for concurrent computation, modal and temporal logics with fixed points and their applications to verification and description of program properties. Tools for Concurrency, the Edinburgh Concurrency Workbench.

Slides

• Applying automata and games to simply typed lambda calculus

• An introduction to deciding higher-order matching

• Dependency tree automata

• lecture one lecture two lecture three lecture four

• lecture one lecture two lecture three lecture four

Books

• 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

Recent Papers

• Proof systems for retracts in simply typed lambda calculus
  Submitted for publication, 2013.

• An introduction to decidability of higher-order matching
  Submitted for publication, 2012.

• 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)