Simon Gay's Publications (by topic)

[ By type | By topic | By year ]

Session Types

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.

Quantum Computing

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.

Interaction Categories

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.

Automated Reasoning

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

Applied Type Theory

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

Types for Pi Calculus

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

Interaction Nets

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.

Other

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.