Guy McCusker's Research Papers and Slides

These documents are in postscript or PDF format, many compressed with gzip.

Back to my home page.

View my research projects.

Imperative Curry-Howard Correspondence

Martin Churchill, Jim Laird and Guy McCusker. Imperative programs as proofs via game semantics. In: 2011 IEEE 26th Annual Symposium on Logic in Computer Science..

Differential lambda-calculus

Jim Laird, Giulio Manzonetto and Guy McCusker. Constructing differential categories and deconstructing categories of games. In: Aceto, L., Henzinger, M. and Sgall, J., eds. Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Proceedings..

Logic Programming

Ekaterina Komendantskaya, John Power and Guy McCusker. Coalgebraic Semantics for Parallel Derivation Strategies in Logic Programming. In: Johnson, M. and Pavlovic, P., eds, Proceedings, Algebraic Methodology and Software Technology, AMAST 2010. Lecture Notes in Computer Science vol. 6486, Springer-Verlag 2011.

Relating game-like models with other models

Guy McCusker and John Power. Modelling Local Variables: Possible Worlds and Object Spaces. In: Selinger, P., ed. Proceedings, Twenty-sixth conference on the Mathematical Foundations of Programming Semantics, MFPS 2010.Elsevier 2010.

Ana Calderon and Guy McCusker. Understanding game semantics through coherence spaces. In: Selinger, P., ed. Proceedings, Twenty-sixth conference on the Mathematical Foundations of Programming Semantics, MFPS 2010.Elsevier 2010.

Bunched implications

Guy McCusker and David Pym. A Games Model of Bunched Implications. In Proceedings, Computer Science Logic (CSL) 2007, volume 4646 of LNCS, copyright © 2007 Springer-Verlag.

Guy McCusker. A Posetal Cartesian Doubly-Closed Category. A very trivial one-page note which takes up two pages of pdf.

Modelling Syntactic Control of Interference

Guy McCusker. Categorical models of Syntactic Control of Interference Revisited, Revisited. LMS J. Comput. Math (10) 176-216, June 2007.

Guy McCusker. A graph model for imperative computation.

Guy McCusker. A fully abstract relational model of Syntactic Control of Interference. In Proceedings, Computer Science Logic (CSL) 2002, volume 2471 of LNCS, copyright © 2002 Springer-Verlag.

Matthew Wall. Games for Syntactic Control of Interference. PhD thesis, supervised by Guy McCusker; the work presented here was joint between the two of us. Available as PDF.

Regular languages and game semantics

Dan R. Ghica and Guy McCusker. The regular language semantics of second-order Idealised Algol. In Theoretical Computer Science 309:469-502, 2003. Available as postscript and PDF, gzipped.

Guy McCusker. Game Semantics of Imperative Languages using Regular Expressions. Slides from the Spring School on Theoretical Computer Science 2002, Agay, France.

The slides are PDF files.

Dan R. Ghica and Guy McCusker. Reasoning about Idealised Algol using regular languages. In Proceedings, Twenty-Seventh International Colloquium on Automata, Languages and Programming (ICALP 2000). Available as postscript and PDF.

Game semantics for nondeterminism

Russell Harmer and Guy McCusker. A fully abstract game semantics for finite nondeterminism. In Proceedings, Fourteenth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1999. Available as postscript.

Marktoberdorf lecture notes

Samson Abramsky and Guy McCusker. Game Semantics. In H. Schwichtenberg and U. Berger, editors, Logic and Computation: Proceedings of the 1997 Marktoberdorf Summer School, Springer-Verlag, 1998.
These notes contain an informal introduction to some of the ideas in game semantics, and an account of full abstraction results for functional languages and extensions with state and control. Available as postscript, and in tree-friendly 2up format (A4 size).

Game semantics for references

Samson Abramsky, Kohei Honda and Guy McCusker. A fully abstract game semantics for general references. In Proceedings, Thirteenth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1998, pages 334-344. Available as postscript.

Call-by-value games

Samson Abramsky and Guy McCusker. Call-by-value games. In M. Nielsen and W. Thomas (eds), Proceedings of CSL '97, Springer-Verlag Lecture Notes in Computer Science, 1998. Available as postscript; an earlier version is available as postscript too.

Game semantics for Algol-like languages

Guy McCusker. On the semantics of the bad-variable constructor in Algol-like languages. In Proceedings, MFPS 2003, Montreal: Electronic Notes in Theoretical Computer Science volume 83, Elsevier 2003. Available from the ENTCS Home Page.

Samson Abramsky and Guy McCusker. Linearity, Sharing and State: a Fully Abstract Game Semantics for Idealized Algol with active expressions (Extended abstract) . In Proceedings of 1996 Linear Logic meeting, Tokyo: Electronic Notes in Theoretical Computer Science volume 3, Elsevier 1996. Because this is an electronic publication, it is not available from here. Go to the ENTCS Home Page to find it.

Samson Abramsky and Guy McCusker. Linearity, Sharing and State: a Fully Abstract Game Semantics for Idealized Algol with active expressions . In O'Hearn and Tennent (eds.), Algol-like languages, Birkhauser 1997. Available as postscript.

Samson Abramsky and Guy McCusker. Full abstraction for Idealized Algol with Passive Expressions. In Theoretical Computer Science, 227:3--42, 1999. Available as postscript.

Game Semantics for Recursive Types

Samson Abramsky and Guy McCusker. Games for Recursive Types. In Proceedings of the Second Workshop of the Theory and Formal Methods Section, Imperial College Department of Computing, IC Press, 1995. Available as postscript.

Samson Abramsky and Guy McCusker. Games and Full Abstraction for the Lazy Lambda Calculus. In Proceedings of 10th annual IEEE symposium on Logic in Computer Science, 1995. Available as postscript.

Guy McCusker. Games and Full Abstraction for FPC (extended abstract). In Proceedings of 11th annual IEEE symposium on Logic in Computer Science, 1996. Available as postscript.

Guy McCusker. Games and Full Abstraction for FPC (full version). In Information and Computation 160, p1-61, 2000. Available as postscript.

Guy McCusker. Games and Full Abstraction for a Functional Metalanguage with Recursive Types. PhD thesis, Imperial College, University of London 1996. Published in Springer-Verlag's Distinguished Dissertations in Computer Science series, 1998. Here is the abstract.

Guy McCusker. Games and Definability for FPC. In Bulletin of Symbolic Logic, 3(3):347-362, September 1997. This paper is available from the BSL page.

Full abstraction by translation

Guy McCusker. Full abstraction by translation. In Advances in Theory and Formal Methods of Computing, IC Press, 1996. Available as postscript.