O. Dardha and S. J. Gay. A New Linear Logic for Deadlock-Free Session-Typed Processes.
In: Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS).
Springer LNCS 10803, 91-109, 2018.
DOI: 10.1007/978-3-319-89366-2_5
D. Kouzapas, O. Dardha, R. Perera and S. J. Gay. Typechecking Protocols with Mungo and StMungo: A Session Type Toolchain for Java.
Science of Computer Programming 155:52-75, 2018.
DOI: j.scico.2017.10.006
S. J. Gay and A. Ravara (editors). Behavioural Types: from Theory to Tools.
River Publishers, 2017.
O. Dardha, S. J. Gay, D. Kouzapas, R. Perera, A. L. Voinea and F. Weber. Mungo and StMungo: Tools for Typechecking Protocols in Java.
In: Behavioural Types: from Theory to Tools (S. J. Gay and A. Ravara, eds.).
River Publishers, 2017.
A. L. Voinea and S. J. Gay. Benefits of session types for software development.
In: Proceedings of the 7th Workshop on Evaluation and Usability of Programming Languages and Tools -- PLATEAU'16.
ACM Press, 2016.
Davide Ancona, Viviana Bono, Mario Bravetti, Giuseppe Castagna, Joana Campos, Simon J. Gay, Elena Giachino, Einar Broch Johnsen, Viviana Mascardi, Nicholas Ng, Luca Padovani, Pierre-Malo Denielou, Nils Gesbert, Raymond Hu, Francisco Martins, Fabrizio Montesi, Rumyana Neykova, Vasco T. Vasconcelos and Nobuko Yoshida. Behavioral Types in Programming Languages
Foundations and Trends in Programming Languages 3(2-3):95-230, 2016.
DOI: 10.1561/2500000031
D. Kouzapas, O. Dardha, R. Perera and S. J. Gay. Typechecking protocols with Mungo and StMungo.
In: Proceedings of the 18th International Symposium on
Principles and Practice of Declarative Programming.
ACM Press, 2016.
DOI:10.1145/2967973.2968595
R. Perera and S. J. Gay.
Liveness for Verification.
Presented at the Workshop on Live Programming Systems (LIVE), 2016.
R. Perera, J. Lange and S. J. Gay.
Multiparty Compatibility for Concurrent Objects.
Presented at the Workshop on Programming Language Approaches to
Communication and Concurrency-Centric Systems (PLACES), 2016.
S. J. Gay. Subtyping supports safe session substitution.
In: A List of Successes that can Change the World: Essays in Honour of Phil Wadler.
Springer
LNCS series, volume 9600, 2016.
S. J. Gay, N. Gesbert, A. Ravara and V. T. Vasconcelos. Modular Session Types for Objects
Logical Methods in Computer Science 11(4:12), 2015.
DOI: 10.2168/LMCS-11(4:12)2015
S. J. Gay, N. Gesbert and A. Ravara.
Session Types as Generic Process Types.
In: Proceedings of the Combined 21st International Workshop on
Expressiveness in Concurrency
and 11th Workshop on
Structural Operational Semantics (EXPRESS/SOS), Electronic Proceedings in Theoretical Computer Science 160:94-110, 2014.
DOI:10.4204/EPTCS.160.9
(Earlier version presented at the Workshop on Programming Language Approaches to
Communication and Concurrency-Centric Systems (PLACES), 2008).
G. Bernardi, O. Dardha, S. J. Gay and D. Kouzapas. On duality relations for session types.
In: Proceedings of the 9th International Symposium on Trustworthy Global Computing (TGC).
Springer
LNCS series, volume 8902, pages 51-66, 2014.
DOI:10.1007/978-3-662-45917-1_4
D. Kouzapas, R. Gutkovas and S. J. Gay.
Session Types for Broadcasting.
Presented at the Workshop on Programming Language Approaches to
Communication and Concurrency-Centric Systems (PLACES), 2014.
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, 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 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 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
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, 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.
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.
E. Ardeshir-Larijani, S. J. Gay and R. Nagarajan. Automated Equivalence Checking of Concurrent Quantum Systems.
ACM Transactions on Computational Logic 19(4):28, 2018.
DOI: 10.1145/3231597
S. J. Gay and I. V. Puthoor. Equational reasoning about quantum protocols.
In: Proceedings of the 7th Conference on Reversible Computation.
Springer
LNCS series, volume 9138, pages 155-172, 2015.
DOI:10.1007/978-3-319-20860-2_10
S. Franke-Arnold, S. J. Gay and I. V. Puthoor. Verification of linear optical quantum computing using quantum process calculus.
In: Proceedings of the Combined 21st International Workshop on
Expressiveness in Concurrency
and 11th Workshop on
Structural Operational Semantics (EXPRESS/SOS), Electronic Proceedings in Theoretical Computer Science 160:111-129, 2014.
DOI:10.4204/EPTCS.160.10
E. Ardeshir-Larijani, S. J. Gay and R. Nagarajan. Verification of Concurrent Quantum Protocols by Equivalence Checking.
In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).
Springer
LNCS series, volume 8413, pages 500-514, 2014.
DOI:10.1007/978-3-642-54862-8_42
S. J. Gay and R. Nagarajan. Techniques for Formal Modelling and Analysis of Quantum Systems.
In: Computation, Logic, Games, and Quantum Foundations: The Many Facets of Samson Abramsky (Essays Dedicated to Samson Abramsky on the Occasion of his 60th Birthday).
Springer
LNCS series,
volume 7860, pages 264-276, 2013.
DOI:10.1007/978-3-642-38164-5_18
S. Franke-Arnold, S. J. Gay and I. V. Puthoor. Quantum process calculus for linear optical quantum computing.
In: Proceedings of the 5th Conference on Reversible Computation.
Springer
LNCS series,
volume 7948, pages 234-246, 2013.
DOI:10.1007/978-3-642-38986-3_19
E. Ardeshir-Larijani, S. J. Gay and R. Nagarajan. Equivalence Checking of Quantum Protocols.
In: Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).
Springer
LNCS series,
volume 7795, pages 466-480, 2013.
DOI:10.1007/978-3-642-36742-7_33
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 95:67-80, 2012.
DOI:10.4204/EPTCS.95.7
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 quant-ph:1112.2156, 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
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, N. Papanikolaou and R. Nagarajan. Model-Checking Quantum Protocols.
August 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. 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 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).
R. Nagarajan and S. J. Gay.
Formal Verification of Quantum Protocols.
arXiv:quant-ph/0203086,
March 2002.
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. 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. 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. 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. Linear Types for Communicating
Processes.
Ph.D. Thesis, Imperial College London, 1995.
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. 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. Cables, Trains and Types.
In: Chris Hankin's Festschrift (to appear), 2019.
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
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 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. 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. Interaction Nets.
Dissertation, Diploma in Computer Science, University of Cambridge
Computer Laboratory, 1991.
M. Gaur, S. J. Gay and I. C. Mackie. A Routing Calculus with Flooding Updates.
In: Proceedings of the 11th International Conference on Distributed Computing and Internet Technology (ICDCIT).
Springer
LNCS series, volume 8956, pages 181-186, 2015.
DOI:10.1007/978-3-319-14977-6_12
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.