Simon Gay's Publications (by year)

[ By type | By topic | By year | By popularity ]

T. Davidson, S. J. Gay, R. Nagarajan and I. V. Puthoor. Analysis of a Quantum Error Correcting Code using Quantum Process Calculus.
In: Proceedings of the International Workshop on Quantum Physics and Logic (QPL 2011).
Electronic Proceedings in Theoretical Computer Science 2012 (to appear).

T. Davidson, S. J. Gay, H. Mlnarik, R. Nagarajan and N. Papanikolaou. Model Checking for Communicating Quantum Processes.
International Journal of Unconventional Computing 8(1):73-98, 2012.

S. J. Gay. Stabilizer States as a Basis for Density Matrices. arXiv, December 2011.

T. Davidson, S. J. Gay and R. Nagarajan. Formal Analysis of Quantum Systems using Process Calculus.
In: Proceedings of the Interaction and Concurrency Experience (ICE).
Electronic Proceedings in Theoretical Computer Science 59:104-110, 2011.
DOI:10.4204/EPTCS.59.9

A. F. Donaldson and S. J. Gay. Type Inference and Strong Static Type Checking for Promela.
Science of Computer Programming 75(11):1165-1191, 2010.
DOI:10.1016/j.scico.2010.05.010

S. J. Gay and V. T. Vasconcelos. Linear Type Theory for Asynchronous Session Types.
Journal of Functional Programming 20(1):19-50, 2010.
Copyright Cambridge University Press. DOI:10.1017/S0956796809990268

S. J. Gay and I. C. Mackie (editors). Semantic Techniques in Quantum Computation.
Cambridge University Press, 2010.

S. J. Gay, R. Nagarajan and N. Papanikolaou. Specification and Verification of Quantum Protocols.
In: Semantic Techniques in Quantum Computation (S. J. Gay and I. C. Mackie, eds.). Cambridge University Press, 2010.

S. J. Gay, V. T. Vasconcelos, A. Ravara, N. Gesbert and A. Z. Caldeira. Modular Session Types for Distributed Object-Oriented Programming
In: Proceedings of the 37th ACM Symposium on Principles of Programming Languages, 2010.
DOI: 10.1145/1706299.1706335
Also Technical Report TR-2010-308, Department of Computing Science, University of Glasgow.
Note: the PDF here is the technical report version, including proofs and some small corrections.

V. T. Vasconcelos, S. J. Gay, A. Ravara, N. Gesbert and A. Z. Caldeira. Dynamic Interfaces.
Presented at the Workshop on Foundations of Object-Oriented Languages (FOOL), January 2009.

S. J. Gay. Bounded polymorphism in session types.
Mathematical Structures in Computer Science, 18(5):895-930, 2008.
DOI:10.1017/S0960129508006944

S. J. Gay, N. Papanikolaou and R. Nagarajan. Model-Checking Quantum Protocols.
August 2008.

S. J. Gay, N. Gesbert and A. Ravara. Session Types as Generic Process Types.
Presented at the Workshop on Programming Language Approaches to Communication and Concurrency-Centric Systems (PLACES), 2008.

S. J. Gay, N. Papanikolaou and R. Nagarajan. QMC: a model checker for quantum systems.
In: Proceedings of the 20th International Conference on Computer Aided Verification (CAV).
Springer LNCS series, volume 5123, pages 543-547, 2008.
DOI:10.1007/978-3-540-70545-1_51
An earlier version is arXiv:0704.3705 and Research Report 432, Department of Computer Science, University of Warwick.

S. J. Gay and V. T. Vasconcelos. Asynchronous Functional Session Types.
Technical report TR-2007-251, Department of Computing Science, University of Glasgow, May 2007.

V. T. Vasconcelos, S. J. Gay and A. Ravara. Type checking a multithreaded functional language with session types.
Revised and expanded version of CONCUR'04.
Theoretical Computer Science 368(1-2):64-87, 2006.
DOI:10.1016/j.tcs.2006.06.028

S. J. Gay. Quantum programming languages: survey and bibliography
Mathematical Structures in Computer Science 16(4):581-600, 2006.
DOI:10.1017/S0960129506005378
Note: In my opinion, the formatting of my version (title link) is preferable to that of the final journal version (DOI link).

S. J. Gay and R. Nagarajan. Types and typechecking for Communicating Quantum Processes
Mathematical Structures in Computer Science 16(3):375-406, 2006.
DOI:10.1017/S0960129506005263

S. J. Gay and M. J. Hole. Subtyping for session types in the pi calculus
Acta Informatica 42(2/3):191-225, 2005.
DOI: 10.1007/s00236-005-0177-z

A. F. Donaldson and S. J. Gay. ETCH: An Enhanced Type Checking Tool for Promela.
In: Proceedings of the SPIN Workshop.
Springer LNCS series, volume 3639, pages 237-242, 2005. Copyright Springer.
DOI: 10.1007/11537328_21

S. J. Gay and R. Nagarajan. Communicating Quantum Processes.
In: Proceedings of the 32nd ACM Symposium on Principles of Programming Languages, 2005.
DOI: 10.1145/1040305.1040318

S. J. Gay, R. Nagarajan and N. Papanikolaou. Probabilistic Model-Checking of Quantum Protocols.
arXiv:quant-ph/0504007, April 2005.

R. Nagarajan, N. Papanikolaou, G. Bowen and S. J. Gay. An Automated Analysis of the Security of Quantum Key Distribution.
arXiv:cs.CR/0502048, February 2005.
Presented at the Workshop on Security Issues in Concurrency (SecCo 2005).

V. T. Vasconcelos, A. Ravara and S. J. Gay. Session Types for Functional Multithreading.
In: Proceedings of the International Conference on Concurrency Theory (CONCUR).
Springer LNCS series, volume 3170, pages 497-511, 2004.
DOI: 10.1007/978-3-540-28644-8_32
Superseded by Theoretical Computer Science 2006.

S. J. Gay and R. Nagarajan. Intensional and Extensional Semantics of Dataflow Programs.
Formal Aspects of Computing 15:299-318, 2003.
DOI: 10.1007/s00165-003-0018-1

S. J. Gay, V. T. Vasconcelos and A. Ravara. Session Types for Inter-Process Communication.
Technical report TR-2003-133, Department of Computing Science, University of Glasgow, March 2003.

M. J. Hole and S. J. Gay. Bounded Polymorphism in Session Types.
Technical report TR-2003-132, Department of Computing Science, University of Glasgow, March 2003.

R. Nagarajan and S. J. Gay. Formal Verification of Quantum Protocols.
arXiv:quant-ph/0203086, March 2002.

S. J. Gay. A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL. Isabelle sources are here.
In: Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001).
Springer LNCS series, volume 2152, pages 217-232, 2001. Copyright Springer.
DOI: 10.1007/3-540-44755-5_16

S. Abramsky, S. J. Gay and R. Nagarajan. A specification structure for deadlock-freedom of synchronous processes.
Theoretical Computer Science 222(1-2):1-53, 1999.
DOI: 10.1016/S0304-3975(98)00189-3

S. J. Gay and M. J. Hole. Types and Subtypes for Client-Server Interactions.
In: Proceedings of the European Symposium on Programming Languages and Systems.
Springer LNCS series, volume 1576, pages 74-90, 1999. Copyright Springer.
DOI: 10.1007/3-540-49099-X_6
Superseded by Acta Informatica 42(2/3):191-225, 2005.

S. Abramsky, S. J. Gay and R. Nagarajan. A Type-Theoretic Approach to Deadlock-Freedom of Asynchronous Systems.
In: Proceedings of the International Symposium on Theoretical Aspects of Computer Software.
Springer LNCS series, volume 1281, pages 295-320, 1997. Copyright Springer.
DOI: 10.1007/BFb0014557

S. J. Gay and C. L. Hankin. Gamma and the Logic of Transition Traces.
In: Advances in Theory and Formal Methods of Computing (A. Edalat, S. Jourdan and G. McCusker, eds.) Imperial College Press, 1997.

S. J. Gay and C. L. Hankin. A Program Logic for Gamma.
In: Coordination Programming: Mechanisms, Models and Semantics (J.-M. Andreoli and C. L. Hankin, eds.) Imperial College Press, 1996.

S. Abramsky, S. J. Gay and R. Nagarajan. Interaction Categories and the Foundations of Typed Concurrent Programming.
In: Deductive Program Design: Proceedings of the 1994 Marktoberdorf Summer School (M. Broy, ed.). NATO ASI Series F, Springer, 1996.

S. Abramsky, S. J. Gay and R. Nagarajan. Specification Structures and Propositions-as-Types for Concurrency.
In: Logics for Concurrency: Structure versus Automata - Proceedings of the VIIIth Banff Higher Order Workshop (G. Birtwistle and F. Moller, eds.). Springer LNCS series, volume 1043, pages 5-40, 1996.
DOI: 10.1007/3-540-60915-6_2

S. J. Gay and R. Nagarajan. A Typed Calculus of Synchronous Processes.
In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, 1995.
DOI: 10.1109/LICS.1995.523258

R. L. Crole, S. J. Gay and R. Nagarajan. An Internal Language for Interaction Categories.
In: Theory and Formal Methods 1994: Proceedings of the Second Imperial College Department of Computing Workshop on Theory and Formal Methods (C. L. Hankin, I. C. Mackie and R. Nagarajan, eds.) Imperial College Press, 1995.

S. J. Gay. Combinators for Interaction Nets.
In: Theory and Formal Methods 1994: Proceedings of the Second Imperial College Department of Computing Workshop on Theory and Formal Methods (C. L. Hankin, I. C. Mackie and R. Nagarajan, eds.) Imperial College Press, 1995.

S. J. Gay. Linear Types for Communicating Processes.
Ph.D. Thesis, Imperial College London, 1995.

S. J. Gay. A Sort Inference Algorithm for the Polyadic Pi-Calculus.
In: Proceedings of the 20th ACM Symposium on Principles of Programming Languages, 1993.
DOI: 10.1145/158511.158701

S. J. Gay and R. Nagarajan. Modelling SIGNAL in Interaction Categories.
In: Theory and Formal Methods 1993: Proceedings of the First Imperial College Department of Computing Workshop on Theory and Formal Methods (G. L. Burn, S. J. Gay and M. D. Ryan, eds.), Workshops in Computing, Springer, 1993.

S. J. Gay. Interaction Nets.
Dissertation, Diploma in Computer Science, University of Cambridge Computer Laboratory, 1991.