Dr Simon Gay

Simon Gay
  • Senior Lecturer (Computing Science)

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

Room S142 Level S
School of Computing Science
Sir Alwyn Williams Building
Glasgow G12 8RZ


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

Biography:
Dr Simon Gay joined the School of Computing Science as a Lecturer in 2000, and became a Senior Lecturer in 2006. Before coming to the University of Glasgow he 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. He has 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.

Dr Gay's research concerns two main areas. The first is foundations of programming languages, especially the topic of type systems for concurrent and distributed programming languages. The second is quantum computing, especially the development of formal verification techniques for systems that combine quantum and classical computation and communication.

Within the School of Computing Science, Dr Gay is a member of the Formal Analysis, Theory and Algorithms (FATA) research group. He is also actively involved in the Scottish Programming Languages Seminar (SPLS) and Quantum Information Scotland (QuISco), and is a member of the Research Committee of the British Computer Society Academy of Computing.

Research Interests:
- Foundations of programming languages
- type systems
- quantum information
- formal verification

Selected publications | View all publications

Gay, S., and Vasconcelos, V. (2010) Linear type theory for asynchronous session types. Journal of Functional Programming, 20 (01). pp. 19-50. ISSN 0956-7968 (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, 17-23 Jan 2010, Madrid, Spain.

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. ISSN 0167-6423 (doi:10.1016/j.scico.2010.05.010)

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

All publications | View selected publications

List all by: Type | Date

Jump to: 2014 | 2013 | 2012 | 2011 | 2010 | 2009 | 2008 | 2006 | 2005 | 2004 | 2003 | 2002 | 2001 | 1999 | 1997 | 1996 | 1995 | 1993
Number of items: 32.

2014

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), 5-13 Apr 2014, Grenoble, France.

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

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

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

2012

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. ISSN 1548-7199

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. Proceedings of the International Workshop on Quantum Physics and Logic (QPL 2011), 95 . pp. 67-80. ISSN 2075-2180 (doi:10.4204/EPTCS.95.7)

2011

Davidson, T.A.S., Gay, S.J., and Nagarajan, R. (2011) Formal analysis of quantum systems using process calculus. Electronic Proceedings in Theoretical Computer Science. Proceedings of the Interaction and Concurrency Experience (ICE), 59 . pp. 104-110. ISSN 2075-2180 (doi:10.4204/EPTCS.59.9)

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. ISSN 0167-6423 (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. ISSN 0956-7968 (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, 17-23 Jan 2010, Madrid, Spain.

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), 24 Jan 2009, Savannah, Georgia, USA.

2008

Gay, S. (2008) Bounded polymorphism in session types. Mathematical Structures in Computer Science, 18 (05). pp. 895-930. ISSN 0960-1295 (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. ISSN 0302-9743 (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. ISSN 0960-1295 (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, 12-14 January 2005, Long Beach, California, USA.

2004

Vasconcelos, V., Ravara, A., and Gay, S. (2004) Session types for functional multithreading. Concur 2004 - Concurrency Theory, Proceedings, 3170 . pp. 497-511.

2003

Gay, S. (2003) Intensional and Extensional Semantics of Dataflow Programs. Formal Aspects of Computing, 15 . pp. 299-318. ISSN 1433-299X (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. ISSN 0302-9743 (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. ISSN 0304-3975 (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. ISSN 0302-9743 (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. ISSN 0302-9743 (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. ISSN 0302-9743 (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, 26-29 Jun 1995, San Diego, CA , USA .

1993

Gay, S. (1993) A sort inference algorithm for the polyadic π-calculus. In: 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1993, Charleston, South Carolina, United States .

This list was generated on Wed Dec 17 12:43:10 2014 GMT.
Number of items: 32.

Articles

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. ISSN 1548-7199

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. Proceedings of the International Workshop on Quantum Physics and Logic (QPL 2011), 95 . pp. 67-80. ISSN 2075-2180 (doi:10.4204/EPTCS.95.7)

Davidson, T.A.S., Gay, S.J., and Nagarajan, R. (2011) Formal analysis of quantum systems using process calculus. Electronic Proceedings in Theoretical Computer Science. Proceedings of the Interaction and Concurrency Experience (ICE), 59 . pp. 104-110. ISSN 2075-2180 (doi:10.4204/EPTCS.59.9)

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. ISSN 0167-6423 (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. ISSN 0956-7968 (doi:10.1017/S0956796809990268)

Gay, S. (2008) Bounded polymorphism in session types. Mathematical Structures in Computer Science, 18 (05). pp. 895-930. ISSN 0960-1295 (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. ISSN 0302-9743 (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. ISSN 0960-1295 (doi:10.1017/S0960129506005378)

Vasconcelos, V., Ravara, A., and Gay, S. (2004) Session types for functional multithreading. Concur 2004 - Concurrency Theory, Proceedings, 3170 . pp. 497-511.

Gay, S. (2003) Intensional and Extensional Semantics of Dataflow Programs. Formal Aspects of Computing, 15 . pp. 299-318. ISSN 1433-299X (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. ISSN 0302-9743 (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. ISSN 0304-3975 (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. ISSN 0302-9743 (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. ISSN 0302-9743 (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. ISSN 0302-9743 (doi:10.1007/3-540-60915-6_2)

Book Sections

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

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

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

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

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), 5-13 Apr 2014, Grenoble, France.

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, 17-23 Jan 2010, Madrid, Spain.

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), 24 Jan 2009, Savannah, Georgia, USA.

Gay, S.J., and Nagarajan, R. (2005) Communicating quantum processes. In: Proceedings of the 32nd ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 12-14 January 2005, Long Beach, California, USA.

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, 26-29 Jun 1995, San Diego, CA , USA .

Gay, S. (1993) A sort inference algorithm for the polyadic π-calculus. In: 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1993, Charleston, South Carolina, United States .

This list was generated on Wed Dec 17 12:43:10 2014 GMT.