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. 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
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 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. 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
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, 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.
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. 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. 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.
Bounded
polymorphism in session types.
Mathematical Structures in Computer Science, 18(5):895-930, 2008.
DOI:10.1017/S0960129508006944
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.
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
S. J. Gay. Linear Types for Communicating
Processes.
Ph.D. Thesis, Imperial College London, 1995.
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. 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 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, 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 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. 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
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).
R. Nagarajan and S. J. Gay.
Formal Verification of Quantum Protocols.
arXiv:quant-ph/0203086,
March 2002.
S. J. Gay, R. Nagarajan and N. Papanikolaou.
Probabilistic Model-Checking of Quantum Protocols.
arXiv:quant-ph/0504007,
April 2005.
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. 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 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.
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.
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. 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. J. Gay. Interaction Nets.
Dissertation, Diploma in Computer Science, University of Cambridge
Computer Laboratory, 1991.
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 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 V. T. Vasconcelos. Asynchronous Functional Session
Types.
Technical
report TR-2007-251, Department of Computing Science, University of
Glasgow, May 2007.
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.
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
S. J. Gay. Stabilizer States as a Basis for Density Matrices. arXiv, December 2011.
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, 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 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 and I. C. Mackie (editors). Semantic Techniques in Quantum Computation.
Cambridge University Press, 2010.
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