Professor Simon Gay

  • Professor, Head of School (Computing Science)

telephone: 01413306035
email: Simon.Gay@glasgow.ac.uk

Room S161A, School of Computing Science, Sir Alwyn Williams Building, University of Glasgow, Glasgow, G12 8QQ

Import to contacts

ORCID iDhttps://orcid.org/0000-0003-3033-9091

Biography

I joined the School of Computing Science as a Lecturer in 2000, becoming a Senior Lecturer in 2006 and a Professor in 2015. I have been Head of School since June 2020.

Before coming to the University of Glasgow I was a Lecturer in Computer Science at Royal Holloway, University of London, and before that, a Research Associate in the Department of Computing at Imperial College London. I have an MA in Pure and Applied Mathematics and a Diploma in Computer Science, both from the University of Cambridge, and a PhD in Computing from Imperial College London.

My main project is "Session Types for Reliable Distributed Systems (STARDUST)", funded by EPSRC. I am also involved in the EU RISE project "BehAPI: Behavioural Application Program Interfaces".

Personal website: http://www.dcs.gla.ac.uk/~simon

Research interests

Research overview

My research concerns two main areas. The first is programming languages: the study of the theory, design and practice of the languages in which computer software is designed and coded. I am particularly interested in designing programming language features to make it easier for programmers to develop software that relies heavily on communication - for example, communication between computers and devices across the internet.

My other research interest is quantum computing, especially the development of techniques for verifying the correctness of systems that combine quantum and classical computation and communication.

Personal website: http://www.dcs.gla.ac.uk/~simon

 

Publications

Selected publications

Dardha, O. , Gay, S. J. , Kouzapas, D., Perera, R. , Voinea, A. L. and Weber, F. (2017) Mungo and StMungo: tools for typechecking protocols in Java. In: Gay, S. and Ravara, A. (eds.) Behavioural Types: from Theory to Tools. Series: River Publishers Series in Automation, Control and Robotics. River Publishers, pp. 309-328. ISBN 9788793519824

Kouzapas, D., Dardha, O. , Perera, R. and Gay, S. J. (2016) Typechecking Protocols with Mungo and StMungo. In: 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016), Edinburgh, UK, 5-7 Sept 2016, pp. 146-159. ISBN 9781450341486 (doi: 10.1145/2967973.2968595)

Gay, S. J. , Gesbert, N., Ravara, A. and Vasconcelos, V. T. (2015) Modular session types for objects. Logical Methods in Computer Science, 11(4), 12. (doi: 10.2168/LMCS-11(4:12)2015)

Bernardi, G., Dardha, O. , Gay, S. and Kouzapas, D. (2014) On duality relations for session types. In: 9th International Symposium on Trustworthy Global Computing (TGC) 2014, Rome, Italy, 5-6 Sep 2014, pp. 51-66. ISBN 9783662459164 (doi: 10.1007/978-3-662-45917-1_4)

Ardeshir-Larijani, E., Gay, S. J. and Nagarajan, R. (2014) Verification of concurrent quantum protocols by equivalence checking. In: 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Grenoble, France, 5-13 Apr 2014, pp. 500-514. (doi: 10.1007/978-3-642-54862-8_42)

All publications

List by: Type | Date

Jump to: 2024 | 2023 | 2022 | 2021 | 2020 | 2019 | 2018 | 2017 | 2016 | 2015 | 2014 | 2013 | 2012 | 2011 | 2010 | 2009 | 2008 | 2006 | 2005 | 2004 | 2003 | 2002 | 2001 | 1999 | 1997 | 1996 | 1995 | 1993
Number of items: 59.

2024

Kouzapas, D., Gutkovas, R. F., Voinea, A. L. and Gay, S. J. (2024) A session type system for asynchronous unreliable broadcast communication. Logical Methods in Computer Science, 20(3), 13:1-13:54. (doi: 10.46298/lmcs-20(3:13)2024)

2023

Fowler, S. , Attard, D. P., Sowul, F., Gay, S. and Trinder, P. (2023) Special delivery: programming with mailbox types. Proceedings of the ACM on Programming Languages, 7(ICFP), 191. (doi: 10.1145/3607832)

Fowler, S. , Attard, D. P., Sowul, F., Gay, S. and Trinder, P. (2023) Artifact for "Special Delivery: Programming with Mailbox Types". [Artefact]

2022

Gay, S. J. , Pocas, D. and Vasconcelos, V. T. (2022) The Different Shades of Infinite Session Types. In: 25th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2022), Munich, Germany, 02-07 Apr 2022, pp. 347-367. ISBN 9783030992521 (doi: 10.1007/978-3-030-99253-8_18)

2021

Harvey, P. , Fowler, S. , Dardha, O. and Gay, S. J. (2021) Multiparty Session Types for Safe Runtime Adaptation in an Actor Language. In: 35th European Conference on Object Oriented Programming (ECOOP 2021), 12-17 Jul 2021, (doi: 10.4230/LIPIcs.ECOOP.2021.10)

Harvey, P. , Fowler, S. , Dardha, O. and Gay, S. J. (2021) Multiparty Session Types for Safe Runtime Adaptation in an Actor Language. [Artefact]

2020

Voinea, A. L. , Dardha, O. and Gay, S. J. (2020) Typechecking Java Protocols with [St]Mungo. In: 40th IFIP WG 6.1 International Conference, FORTE 2020, Valletta, Malta, 15-19 Jun 2020, pp. 208-224. ISBN 9783030500856 (doi: 10.1007/978-3-030-50086-3_12)

Gay, S. J. (2020) Cables, trains and types. Lecture Notes in Computer Science, 12065, pp. 3-16. (doi: 10.1007/978-3-030-41103-9_1)

2019

Voinea, A. L. , Dardha, O. and Gay, S. J. (2019) Resource Sharing via Capability-Based Multiparty Session Types. In: 15th International Conference on integrated Formal Methods (iFM 2019), Bergen, Norway, 02-06 Dec 2019, pp. 437-455. ISBN 9783030349677 (doi: 10.1007/978-3-030-34968-4_24)

2018

Ardeshir-Larijani, E., Gay, S. J. and Nagarajan, R. (2018) Automated equivalence checking of concurrent quantum systems. ACM Transactions on Computational Logic, 19(4), 28. (doi: 10.1145/3231597)

Kouzapas, D., Dardha, O. , Perera, R. and Gay, S. J. (2018) Typechecking protocols with Mungo and StMungo: a session type toolchain for Java. Science of Computer Programming, 155, pp. 52-75. (doi: 10.1016/j.scico.2017.10.006)

Dardha, O. and Gay, S. J. (2018) A New Linear Logic for Deadlock-Free Session-Typed Processes. In: 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Thessaloniki, Greece, 16-19 Apr 2018, pp. 91-109. (doi: 10.1007/978-3-319-89366-2_5)

2017

Gay, S. and Ravara, A. eds. (2017) Behavioural Types: from Theory to Tools. Series: River Publishers series in automation, control and robotics. River Publishers. ISBN 9788793519824

Dardha, O. , Gay, S. J. , Kouzapas, D., Perera, R. , Voinea, A. L. and Weber, F. (2017) Mungo and StMungo: tools for typechecking protocols in Java. In: Gay, S. and Ravara, A. (eds.) Behavioural Types: from Theory to Tools. Series: River Publishers Series in Automation, Control and Robotics. River Publishers, pp. 309-328. ISBN 9788793519824

2016

Kouzapas, D., Dardha, O. , Perera, R. and Gay, S. J. (2016) Typechecking Protocols with Mungo and StMungo. In: 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016), Edinburgh, UK, 5-7 Sept 2016, pp. 146-159. ISBN 9781450341486 (doi: 10.1145/2967973.2968595)

Perera, R. , Lange, J. and Gay, S. J. (2016) Multiparty Compatibility for Concurrent Objects. In: Ninth Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES 2016), Eindhoven, The Netherlands, 8 Apr 2016, (doi: 10.4204/EPTCS.211.8)

Gay, S. J. (2016) Subtyping supports safe session substitution. Lecture Notes in Computer Science, 9600, pp. 95-108. (doi: 10.1007/978-3-319-30936-1_5)

Gay, S. J. and Ravara, A. (2016) Behavioural Types Part 1 [Guest Editors]. Mathematical Structures in Computer Science, 26(2),

Gay, S. J. and Ravara, A. (2016) Preface to special issue: behavioural types. Mathematical Structures in Computer Science, 26(2), pp. 154-155. (doi: 10.1017/S0960129514000152)

Ancona, D. et al. (2016) Behavioral types in programming languages. Foundations and Trends in Programming Languages, 3(2-3), pp. 95-230. (doi: 10.1561/2500000031)

Voinea, A. L. and Gay, S. J. (2016) Benefits of Session Types for software Development. In: 7th International Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU), Amsterdam, Netherlands, 01 Nov 2016, pp. 26-29. ISBN 9781450346382 (doi: 10.1145/3001878.3001883)

2015

Gay, S. J. , Gesbert, N., Ravara, A. and Vasconcelos, V. T. (2015) Modular session types for objects. Logical Methods in Computer Science, 11(4), 12. (doi: 10.2168/LMCS-11(4:12)2015)

Gaur, M., Gay, S. J. and Mackie, I. (2015) A routing calculus with flooding updates. Lecture Notes in Computer Science, 8956, pp. 181-186. (doi: 10.1007/978-3-319-14977-6_12)

Gay, S. J. and Puthoor, I. V. (2015) Equational reasoning about quantum protocols. Lecture Notes in Computer Science, 9138, pp. 155-170. (doi: 10.1007/978-3-319-20860-2_10)

2014

Bernardi, G., Dardha, O. , Gay, S. and Kouzapas, D. (2014) On duality relations for session types. In: 9th International Symposium on Trustworthy Global Computing (TGC) 2014, Rome, Italy, 5-6 Sep 2014, pp. 51-66. ISBN 9783662459164 (doi: 10.1007/978-3-662-45917-1_4)

Gay, S. J. , Gesbert, N. and Ravara, A. (2014) Session types as generic process types. Electronic Proceedings in Theoretical Computer Science, 160, pp. 94-110. (doi: 10.4204/EPTCS.160.9)

Ardeshir-Larijani, E., Gay, S. J. and Nagarajan, R. (2014) Verification of concurrent quantum protocols by equivalence checking. In: 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Grenoble, France, 5-13 Apr 2014, pp. 500-514. (doi: 10.1007/978-3-642-54862-8_42)

Franke-Arnold, S. , Gay, S. J. and Puthoor, I. V. (2014) Verification of linear optical quantum computing using quantum process calculus. Electronic Proceedings in Theoretical Computer Science, 160, pp. 111-129. (doi: 10.4204/EPTCS.160.10)

Kouzapas, D., Gutkovas, R. and Gay, S. J. (2014) Session Types for Broadcasting. In: 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, Grenoble, France, 12 Apr 2014, pp. 25-31. (doi: 10.4204/EPTCS.155.4)

2013

Ardeshir-Larijani, E., Gay, S. and Nagarajan, R. (2013) Equivalence checking of quantum protocols. In: Piterman, N. and Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems: Proceedings of the 19th International Conference, TACAS 2013, Rome, Italy,16-24 March 2013. Series: Lecture notes in computer science, 7795. Springer Heidelberg: Dordrecht, The Netherlands, pp. 478-492. ISBN 9783642367410 (doi: 10.1007/978-3-642-36742-7_33)

Franke-Arnold, S. , Gay, S.J. and Puthoor, I. (2013) Quantum process calculus for linear optical quantum computing. In: Dueck, G.W. and Miller, M. (eds.) Reversible Computation: Proceedings of the 5th International Conference, RC 2013, Victoria, BC, Canada, 4-5 July 2013. Series: Lecture notes in computer science, 7948. Springer Heidelberg: Dordrecht, The Netherlands, pp. 234-246. ISBN 9783642389856 (doi: 10.1007/978-3-642-38986-3_19)

Gay, S.J. and Nagarajan, R. (2013) Techniques for formal modelling and analysis of quantum systems. In: Coecke, B. and Ong, L. (eds.) Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky: Essays Dedicated to Samson Abramsky on the Occasion of His 60th Birthday. Series: Lecture notes in computer science, 7860. Springer Heidelberg: Dordrecht, The Netherlands, pp. 264-276. ISBN 9783642381638 (doi: 10.1007/978-3-642-38164-5_18)

2012

Davidson, T.A.S., Gay, S.J. , Nagarajan, R. and Puthoor, I.V. (2012) Analysis of a quantum error correcting code using quantum process calculus. Electronic Proceedings in Theoretical Computer Science, 95, pp. 67-80. (doi: 10.4204/EPTCS.95.7)

Davidson, T., Gay, S.J. , Mlnarik, H., Nagarajan, R. and Papanikolaou, N. (2012) Model checking for communicating quantum processes. Journal of Unconventional Computing, 8(1), pp. 73-98.

2011

Gay, S.J. (2011) Stabilizer states as a basis for density matrices. (Unpublished)

2010

Donaldson, A.F. and Gay, S.J. (2010) Type inference and strong static type checking for Promela. Science of Computer Programming, 75(11), pp. 1165-1191. (doi: 10.1016/j.scico.2010.05.010)

Gay, S. and Mackie, I. (Eds.) (2010) Semantic techniques in Quantum Computation. Cambridge University Press: Cambridge. ISBN 9780521513746

Gay, S. , Nagarajan, R. and Papanikolaou, N. (2010) Specification and verification of quantum protocols. In: Gay, S. and Mackie, I. (eds.) Semantic Techniques in Quantum Computation. Cambridge University Press, pp. 414-472. ISBN 9780521513746

Gay, S. and Vasconcelos, V. (2010) Linear type theory for asynchronous session types. Journal of Functional Programming, 20(01), pp. 19-50. (doi: 10.1017/S0956796809990268)

Gay, S. , Vasconcelos, V., Ravara, A., Gesbert, N. and Caldeira, A. (2010) Modular session types for distributed object-oriented programming. In: 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Madrid, Spain, 17-23 Jan 2010, pp. 299-312. ISBN 9781605584799 (doi: 10.1145/1706299.1706335)

2009

Vasconcelos, V.T., Gay, S.J. , Ravara, A., Gesbert, N. and Caldiera, A.Z. (2009) Dynamic interfaces. In: 2009 International Workshop on Foundations of Object-Oriented Languages (FOOL'09), Savannah, Georgia, USA, 24 Jan 2009,

2008

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

Gay, S. , Nagarajan, R. and Papanikolaou, N. (2008) QMC: A Model Checker for Quantum Systems. Lecture Notes in Computer Science, 5123, pp. 543-547. (doi: 10.1007/978-3-540-70545-1_51)

2006

Gay, S. and Nagarajan, R. (2006) Types and typechecking for communicating quantum processes. Mathematical Structures in Computer Science, 16, pp. 375-406. (doi: 10.1017/S0960129506005263)

Vasconcelos, V., Gay, S. and Ravara, A. (2006) Type checking a multithreaded functional language with session types. Theoretical Computer Science, 368, pp. 64-87. (doi: 10.1016/j.tcs.2006.06.028)

2005

Donaldson, A. and Gay, S. (2005) ETCH: An enhanced type checking tool for promela. Model Checking Software, Proceedings, 3639, pp. 266-271.

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

Gay, S. (2005) Quantum programming languages: survey and bibliography. Mathematical Structures in Computer Science, 16(4), pp. 581-600. (doi: 10.1017/S0960129506005378)

Gay, S.J. and Nagarajan, R. (2005) Communicating quantum processes. In: Proceedings of the 32nd ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Long Beach, California, USA, 12-14 January 2005, pp. 145-157. ISBN 158113830X (doi: 10.1145/1040305.1040318)

2004

Vasconcelos, V., Ravara, A. and Gay, S. (2004) Session types for functional multithreading. Lecture Notes in Computer Science, 3170, pp. 497-511.

2003

Gay, S. (2003) Intensional and Extensional Semantics of Dataflow Programs. Formal Aspects of Computing, 15, pp. 299-318. (doi: 10 1007/s00165-003-0018-1)

2002

Gay, S. (2002) Formal verification of quantum protocols.

2001

Gay, S.J. (2001) A framework for the formalisation of Pi calculus type systems in Isabelle/HOL. Lecture Notes in Computer Science, 2152, pp. 217-232. (doi: 10.1007/3-540-44755-5_16)

1999

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

Gay, S. and Hole, M. (1999) Types and subtypes for client-server interactions. Lecture Notes in Computer Science, 1576, pp. 74-90. (doi: 10.1007/3-540-49099-X_6)

1997

Abramsky, S., Gay, S. and Nagarajan, R. (1997) A type-theoretic approach to deadlock-freedom of asynchronous systems. Lecture Notes in Computer Science, 1281, p. 295. (doi: 10.1007/BFb0014557)

1996

Abramsky, S., Gay, S. and Nagarajan, R. (1996) Specification structures and propositions-as-types for concurrency. Lecture Notes in Computer Science, pp. 5-40. (doi: 10.1007/3-540-60915-6_2)

1995

Gay, S. and Nagarajan, R. (1995) A typed calculus of synchronous processes. In: Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95, San Diego, CA , USA, 26-29 Jun 1995, pp. 210-220. ISBN 0818670509 (doi: 10.1109/LICS.1995.523258)

1993

Gay, S. (1993) A sort inference algorithm for the polyadic π-calculus. In: 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, United States, 1993, pp. 429-438. ISBN 0897915607 (doi: 10.1145/158511.158701)

This list was generated on Wed Nov 20 19:50:11 2024 GMT.
Number of items: 59.

Articles

Kouzapas, D., Gutkovas, R. F., Voinea, A. L. and Gay, S. J. (2024) A session type system for asynchronous unreliable broadcast communication. Logical Methods in Computer Science, 20(3), 13:1-13:54. (doi: 10.46298/lmcs-20(3:13)2024)

Fowler, S. , Attard, D. P., Sowul, F., Gay, S. and Trinder, P. (2023) Special delivery: programming with mailbox types. Proceedings of the ACM on Programming Languages, 7(ICFP), 191. (doi: 10.1145/3607832)

Gay, S. J. (2020) Cables, trains and types. Lecture Notes in Computer Science, 12065, pp. 3-16. (doi: 10.1007/978-3-030-41103-9_1)

Ardeshir-Larijani, E., Gay, S. J. and Nagarajan, R. (2018) Automated equivalence checking of concurrent quantum systems. ACM Transactions on Computational Logic, 19(4), 28. (doi: 10.1145/3231597)

Kouzapas, D., Dardha, O. , Perera, R. and Gay, S. J. (2018) Typechecking protocols with Mungo and StMungo: a session type toolchain for Java. Science of Computer Programming, 155, pp. 52-75. (doi: 10.1016/j.scico.2017.10.006)

Gay, S. J. (2016) Subtyping supports safe session substitution. Lecture Notes in Computer Science, 9600, pp. 95-108. (doi: 10.1007/978-3-319-30936-1_5)

Gay, S. J. and Ravara, A. (2016) Behavioural Types Part 1 [Guest Editors]. Mathematical Structures in Computer Science, 26(2),

Gay, S. J. and Ravara, A. (2016) Preface to special issue: behavioural types. Mathematical Structures in Computer Science, 26(2), pp. 154-155. (doi: 10.1017/S0960129514000152)

Ancona, D. et al. (2016) Behavioral types in programming languages. Foundations and Trends in Programming Languages, 3(2-3), pp. 95-230. (doi: 10.1561/2500000031)

Gay, S. J. , Gesbert, N., Ravara, A. and Vasconcelos, V. T. (2015) Modular session types for objects. Logical Methods in Computer Science, 11(4), 12. (doi: 10.2168/LMCS-11(4:12)2015)

Gaur, M., Gay, S. J. and Mackie, I. (2015) A routing calculus with flooding updates. Lecture Notes in Computer Science, 8956, pp. 181-186. (doi: 10.1007/978-3-319-14977-6_12)

Gay, S. J. and Puthoor, I. V. (2015) Equational reasoning about quantum protocols. Lecture Notes in Computer Science, 9138, pp. 155-170. (doi: 10.1007/978-3-319-20860-2_10)

Gay, S. J. , Gesbert, N. and Ravara, A. (2014) Session types as generic process types. Electronic Proceedings in Theoretical Computer Science, 160, pp. 94-110. (doi: 10.4204/EPTCS.160.9)

Franke-Arnold, S. , Gay, S. J. and Puthoor, I. V. (2014) Verification of linear optical quantum computing using quantum process calculus. Electronic Proceedings in Theoretical Computer Science, 160, pp. 111-129. (doi: 10.4204/EPTCS.160.10)

Davidson, T.A.S., Gay, S.J. , Nagarajan, R. and Puthoor, I.V. (2012) Analysis of a quantum error correcting code using quantum process calculus. Electronic Proceedings in Theoretical Computer Science, 95, pp. 67-80. (doi: 10.4204/EPTCS.95.7)

Davidson, T., Gay, S.J. , Mlnarik, H., Nagarajan, R. and Papanikolaou, N. (2012) Model checking for communicating quantum processes. Journal of Unconventional Computing, 8(1), pp. 73-98.

Gay, S.J. (2011) Stabilizer states as a basis for density matrices. (Unpublished)

Donaldson, A.F. and Gay, S.J. (2010) Type inference and strong static type checking for Promela. Science of Computer Programming, 75(11), pp. 1165-1191. (doi: 10.1016/j.scico.2010.05.010)

Gay, S. and Vasconcelos, V. (2010) Linear type theory for asynchronous session types. Journal of Functional Programming, 20(01), pp. 19-50. (doi: 10.1017/S0956796809990268)

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

Gay, S. , Nagarajan, R. and Papanikolaou, N. (2008) QMC: A Model Checker for Quantum Systems. Lecture Notes in Computer Science, 5123, pp. 543-547. (doi: 10.1007/978-3-540-70545-1_51)

Gay, S. and Nagarajan, R. (2006) Types and typechecking for communicating quantum processes. Mathematical Structures in Computer Science, 16, pp. 375-406. (doi: 10.1017/S0960129506005263)

Vasconcelos, V., Gay, S. and Ravara, A. (2006) Type checking a multithreaded functional language with session types. Theoretical Computer Science, 368, pp. 64-87. (doi: 10.1016/j.tcs.2006.06.028)

Donaldson, A. and Gay, S. (2005) ETCH: An enhanced type checking tool for promela. Model Checking Software, Proceedings, 3639, pp. 266-271.

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

Gay, S. (2005) Quantum programming languages: survey and bibliography. Mathematical Structures in Computer Science, 16(4), pp. 581-600. (doi: 10.1017/S0960129506005378)

Vasconcelos, V., Ravara, A. and Gay, S. (2004) Session types for functional multithreading. Lecture Notes in Computer Science, 3170, pp. 497-511.

Gay, S. (2003) Intensional and Extensional Semantics of Dataflow Programs. Formal Aspects of Computing, 15, pp. 299-318. (doi: 10 1007/s00165-003-0018-1)

Gay, S. (2002) Formal verification of quantum protocols.

Gay, S.J. (2001) A framework for the formalisation of Pi calculus type systems in Isabelle/HOL. Lecture Notes in Computer Science, 2152, pp. 217-232. (doi: 10.1007/3-540-44755-5_16)

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

Gay, S. and Hole, M. (1999) Types and subtypes for client-server interactions. Lecture Notes in Computer Science, 1576, pp. 74-90. (doi: 10.1007/3-540-49099-X_6)

Abramsky, S., Gay, S. and Nagarajan, R. (1997) A type-theoretic approach to deadlock-freedom of asynchronous systems. Lecture Notes in Computer Science, 1281, p. 295. (doi: 10.1007/BFb0014557)

Abramsky, S., Gay, S. and Nagarajan, R. (1996) Specification structures and propositions-as-types for concurrency. Lecture Notes in Computer Science, pp. 5-40. (doi: 10.1007/3-540-60915-6_2)

Books

Gay, S. and Ravara, A. eds. (2017) Behavioural Types: from Theory to Tools. Series: River Publishers series in automation, control and robotics. River Publishers. ISBN 9788793519824

Book Sections

Dardha, O. , Gay, S. J. , Kouzapas, D., Perera, R. , Voinea, A. L. and Weber, F. (2017) Mungo and StMungo: tools for typechecking protocols in Java. In: Gay, S. and Ravara, A. (eds.) Behavioural Types: from Theory to Tools. Series: River Publishers Series in Automation, Control and Robotics. River Publishers, pp. 309-328. ISBN 9788793519824

Ardeshir-Larijani, E., Gay, S. and Nagarajan, R. (2013) Equivalence checking of quantum protocols. In: Piterman, N. and Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems: Proceedings of the 19th International Conference, TACAS 2013, Rome, Italy,16-24 March 2013. Series: Lecture notes in computer science, 7795. Springer Heidelberg: Dordrecht, The Netherlands, pp. 478-492. ISBN 9783642367410 (doi: 10.1007/978-3-642-36742-7_33)

Franke-Arnold, S. , Gay, S.J. and Puthoor, I. (2013) Quantum process calculus for linear optical quantum computing. In: Dueck, G.W. and Miller, M. (eds.) Reversible Computation: Proceedings of the 5th International Conference, RC 2013, Victoria, BC, Canada, 4-5 July 2013. Series: Lecture notes in computer science, 7948. Springer Heidelberg: Dordrecht, The Netherlands, pp. 234-246. ISBN 9783642389856 (doi: 10.1007/978-3-642-38986-3_19)

Gay, S.J. and Nagarajan, R. (2013) Techniques for formal modelling and analysis of quantum systems. In: Coecke, B. and Ong, L. (eds.) Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky: Essays Dedicated to Samson Abramsky on the Occasion of His 60th Birthday. Series: Lecture notes in computer science, 7860. Springer Heidelberg: Dordrecht, The Netherlands, pp. 264-276. ISBN 9783642381638 (doi: 10.1007/978-3-642-38164-5_18)

Gay, S. , Nagarajan, R. and Papanikolaou, N. (2010) Specification and verification of quantum protocols. In: Gay, S. and Mackie, I. (eds.) Semantic Techniques in Quantum Computation. Cambridge University Press, pp. 414-472. ISBN 9780521513746

Edited Books

Gay, S. and Mackie, I. (Eds.) (2010) Semantic techniques in Quantum Computation. Cambridge University Press: Cambridge. ISBN 9780521513746

Conference Proceedings

Gay, S. J. , Pocas, D. and Vasconcelos, V. T. (2022) The Different Shades of Infinite Session Types. In: 25th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2022), Munich, Germany, 02-07 Apr 2022, pp. 347-367. ISBN 9783030992521 (doi: 10.1007/978-3-030-99253-8_18)

Harvey, P. , Fowler, S. , Dardha, O. and Gay, S. J. (2021) Multiparty Session Types for Safe Runtime Adaptation in an Actor Language. In: 35th European Conference on Object Oriented Programming (ECOOP 2021), 12-17 Jul 2021, (doi: 10.4230/LIPIcs.ECOOP.2021.10)

Voinea, A. L. , Dardha, O. and Gay, S. J. (2020) Typechecking Java Protocols with [St]Mungo. In: 40th IFIP WG 6.1 International Conference, FORTE 2020, Valletta, Malta, 15-19 Jun 2020, pp. 208-224. ISBN 9783030500856 (doi: 10.1007/978-3-030-50086-3_12)

Voinea, A. L. , Dardha, O. and Gay, S. J. (2019) Resource Sharing via Capability-Based Multiparty Session Types. In: 15th International Conference on integrated Formal Methods (iFM 2019), Bergen, Norway, 02-06 Dec 2019, pp. 437-455. ISBN 9783030349677 (doi: 10.1007/978-3-030-34968-4_24)

Dardha, O. and Gay, S. J. (2018) A New Linear Logic for Deadlock-Free Session-Typed Processes. In: 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Thessaloniki, Greece, 16-19 Apr 2018, pp. 91-109. (doi: 10.1007/978-3-319-89366-2_5)

Kouzapas, D., Dardha, O. , Perera, R. and Gay, S. J. (2016) Typechecking Protocols with Mungo and StMungo. In: 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016), Edinburgh, UK, 5-7 Sept 2016, pp. 146-159. ISBN 9781450341486 (doi: 10.1145/2967973.2968595)

Perera, R. , Lange, J. and Gay, S. J. (2016) Multiparty Compatibility for Concurrent Objects. In: Ninth Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES 2016), Eindhoven, The Netherlands, 8 Apr 2016, (doi: 10.4204/EPTCS.211.8)

Voinea, A. L. and Gay, S. J. (2016) Benefits of Session Types for software Development. In: 7th International Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU), Amsterdam, Netherlands, 01 Nov 2016, pp. 26-29. ISBN 9781450346382 (doi: 10.1145/3001878.3001883)

Bernardi, G., Dardha, O. , Gay, S. and Kouzapas, D. (2014) On duality relations for session types. In: 9th International Symposium on Trustworthy Global Computing (TGC) 2014, Rome, Italy, 5-6 Sep 2014, pp. 51-66. ISBN 9783662459164 (doi: 10.1007/978-3-662-45917-1_4)

Ardeshir-Larijani, E., Gay, S. J. and Nagarajan, R. (2014) Verification of concurrent quantum protocols by equivalence checking. In: 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Grenoble, France, 5-13 Apr 2014, pp. 500-514. (doi: 10.1007/978-3-642-54862-8_42)

Kouzapas, D., Gutkovas, R. and Gay, S. J. (2014) Session Types for Broadcasting. In: 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, Grenoble, France, 12 Apr 2014, pp. 25-31. (doi: 10.4204/EPTCS.155.4)

Gay, S. , Vasconcelos, V., Ravara, A., Gesbert, N. and Caldeira, A. (2010) Modular session types for distributed object-oriented programming. In: 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Madrid, Spain, 17-23 Jan 2010, pp. 299-312. ISBN 9781605584799 (doi: 10.1145/1706299.1706335)

Vasconcelos, V.T., Gay, S.J. , Ravara, A., Gesbert, N. and Caldiera, A.Z. (2009) Dynamic interfaces. In: 2009 International Workshop on Foundations of Object-Oriented Languages (FOOL'09), Savannah, Georgia, USA, 24 Jan 2009,

Gay, S.J. and Nagarajan, R. (2005) Communicating quantum processes. In: Proceedings of the 32nd ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Long Beach, California, USA, 12-14 January 2005, pp. 145-157. ISBN 158113830X (doi: 10.1145/1040305.1040318)

Gay, S. and Nagarajan, R. (1995) A typed calculus of synchronous processes. In: Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95, San Diego, CA , USA, 26-29 Jun 1995, pp. 210-220. ISBN 0818670509 (doi: 10.1109/LICS.1995.523258)

Gay, S. (1993) A sort inference algorithm for the polyadic π-calculus. In: 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, United States, 1993, pp. 429-438. ISBN 0897915607 (doi: 10.1145/158511.158701)

Artefact

Fowler, S. , Attard, D. P., Sowul, F., Gay, S. and Trinder, P. (2023) Artifact for "Special Delivery: Programming with Mailbox Types". [Artefact]

Harvey, P. , Fowler, S. , Dardha, O. and Gay, S. J. (2021) Multiparty Session Types for Safe Runtime Adaptation in an Actor Language. [Artefact]

This list was generated on Wed Nov 20 19:50:11 2024 GMT.

Grants

Current projects:

Past projects:

 

Supervision