# home

I am a Senior Lecturer at the School of Electronic Engineering and Computer Science at Queen Mary University of London, and member of the Theory Group. Previously, I was a postdoctoral researcher at the Department of Computer Science at the University of Oxford, and member of the Quantum Group, where I also completed my PhD thesis.

My focus is on Theoretical Computer Science and in particular I study the mathematical meaning of computation. I devise mathematical models of programming languages, expressed in game semantics at the concrete level and in category theory at the abstract level. I examine applications of these models to program analysis in order to develop methods and tools for formally analysing and checking software.

I can be reached at:

nikos.tzevelekos at qmul.ac.uk

tel.: +44 (0)20 7882 6974

School of Electronic Engineering and Computer Science

Queen Mary University of London, London E1 4NS, UK

Office: CS 434

**Events:**

Dagstuhl seminar on Program Equivalence, Highlights 2018, MOVEP 2018, MFGR 2018

FOSSACS 2016, Program Equivalence, Automata, Logic and Games @IMS, Compositionality @Simons

SR 2015, CONCUR 2015, ESSLLI 2015, LOLA 2015, MFPS31, PLS10, GALOP X

ETAPS 2015, Semantics and Verification of Object-Oriented Languages @Shonan

Joint-theory-seminars mailing list (subscribe for seminar announcements in the London area!)

Activities

01/02/20. Our tool

**mokapot**has now its website launched!06/04/19. Talk by Yu-Yang Lin on

*A Bounded Model Checking Technique for Higher-Order Programs*at SETTA'1930/11/19. Talk on

*DEQ : Equivalence Checker for Deterministic Register Automata*at ATVA'1916/08/19. Summer school course on

*Game Semantics*at ESSLLI 201906/04/19. Talk by Yu-Yang Lin on

*A Framework for Compositional Model Checking*at the GALOP workshop @ ETAPS'1919/08/18. Summer school lecture on Automata over Infinite Alphabets at the MOVEP'18 summer school

08/07/18. Talk on

*Game Semantics 25 years on*at the Games 25 workshop @ FLOC'1828/06/18. Talk on

*Nominal game semantics*at the First Congress of Greek Mathematicians14/04/18. Talk on

*An overview of game semantics for polymorphism*at the GALOP workshop @ ETAPS'1810/04/18. Talk on

*Nominal games: a semantics paradigm for effectful languages*at the Dagstuhl seminar on Program Equivalence08/12/16. Gave a talk on

*Higher-Order Linearisability*at the Compositionality workshop, Simons Institute, Berkeley30/11/16. Gave a talk on

*Automata over infinite alphabets: automata with registers and histories*at the Verification Seminar, University of Oxford21/11/16. Gave a talk on

*Nominal games: a semantics paradigm for effectful languages*at the PLAS Seminar, University of Kent10/06/16. Gave a talk on

*Nominal games: a semantics paradigm for effectful languages*at the IMS Workshop on Higher-Order Model Checking + Communicating, Distributed and Parameterised Systems10/06/16. New EPSRC project on System-Level Game Semantics: A unifying framework for composing systems jointly with Dan Ghica

12/04/16. Organised a Workshop on Program Equivalence jointly with Andzej Murawski and Ofer Strichman

13/04/16. Gave a talk on

*Model Checking Program Equivalence in Interface Middleweight Java*at the PPLV seminar at UCL17/03/16. Gave a talk on

*Model Checking Program Equivalence in Interface Middleweight Java*at the NII Shonan meeting on Higher-Order Model Checking26/01/16. Gave a talk on

*History-Register Automata*at the Warwick DIMAP seminar17/11/15. Gave a talk on

*Automata over infinite alphabets: Investigations in Fresh-Register Automata*at Logical Foundations of Data Science13/10/15. Gave a talk on

*Game Semantic Analysis of Equivalence in Interface Middleweight Java*at ATVA'1530/09/15. Gave a talk on

*Automata over infinite alphabets: Investigations in Fresh-Register Automata*at University of Southampton25/09/15. Organised a NII Shonan meeting on Semantics and Verification of OO Languages jointly with Atsushi Igarashi and Andzej Murawski

18/09/15. Gave a talk on Bisimilarity in Fresh-Register Automata at Highlights 2015

07/08/15. Gave joint summer school course on Automata over Infinite Alphabets at ESSLLI 2015

05/07/15. Gave a talk on Nominal games: a low-level semantics for open programs at LOLA 2015

22/06/15. Gave a talk on Game Semantic Analysis of Equivalence in Interface Middleweight Java at MFPS XXXI

16/06/15. CONEQCT will be presented in ATVA 2015. More about the tool at its webpage:

Coneqct: a contextual equivalence checking tool for Interface Middleweight Java

13/06/15. Gave a talk on Automata over infinite alphabets: Investigations in Fresh-Register Automata at PLS10

12/04/15. Gave a talk on Nominal game semantics: what's new at the GALOP 2015 workshop

27/02/15. Gave a talk on Automata over infinite alphabets: Investigations in Fresh-Register Automata at University of Birmingham

19/02/15. Gave a talk on Nominal game semantics and automata at Aarhus University

09/12/14. Gave a talk on Nominal game semantics and automata at Microsoft Research, Cambridge

24/10/14. Gave a talk on Automata (&#59 programs) over infinite alphabets at the OASIS 10 Year Anniversary Workshop, Oxford

03/09/14. Presented joint work with Andrzej Murawski and Steven Ramsey on Reachability in Pushdown Register Automata at the Highlights of Logic, Games and Automata conference, Paris

30/06/14. New EPSRC project on Program Reasoning with Nominal Game Semantics

12/06/14. Gave a talk on Nominal game semantics and automata at the Semantics of proofs and programs workshop, IHP, Paris

26/05/14. Visiting the Institute Henri Poincare for a month, taking part in the Semantics of proofs and certified mathematics trimester

12/04/14. Gave a talk on Game Semantics for Interface Midleweight Java at the GALOP 2014 workshop

09/04/14. Presented joint paper with Andrzej Murawski at FOSSACS 2014

24/01/14. Presented joint paper with Andrzej Murawski at POPL 2014

27/12/13. Gave a talk on Games and Full Abstraction for Java programs at the Programming Languages Seminar, National Technical University of Athens

15/10/13. Gave a tutorial talk on Names, games and automata at the Nominal Computation Theory seminar at Dagstuhl

19/07/13. Gave a talk on Deconstructing general references using game semantics at the HOPE workshop, (ICFP'13 satellite)

30/05/13. Presented joint paper with Andrzej Murawski at the Samson@60 Workshop

12/04/13. Gave a course on

*Typed Lambda Calculus*at the Midlands Graduate School 2013. The slides for the course are hereETAPS 2015 will be held at Queen Mary!

The local organisation will be done by the Theory group, with co-chairs Pasquale Malacaria and myself

18/03/13. Presented joint paper with Radu Grigore on History-Register Automata at FOSSACS'13

08/03/13. Co-chair of GALOP 2013, which is going to be held at Queen Mary, on 18-19 July 2013

18/02/13. PC member of LOLA 2013

27/12/12. Gave a talk on Games with names at the Programming Languages Seminar, National Technical University of Athens

16/12/12. The following joint papers will appear in ETAPS'13

Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen and Nikos Tzevelekos. Runtime Verification Based on Register Automata. (TACAS)

Andrzej Murawski and Nikos Tzevelekos. Deconstructing general references via game semantics. (FOSSACS)

Nikos Tzevelekos and Radu Grigore. History-Register Automata. (FOSSACS)

20/09/12. Organiser, along with Edmund Robinson, of the 17th Wessex Theory Seminar. If you would like to attend, it would be good to contact us so that we know numbers. Registration is free

29/06/12. Gave a talk on Game semantics for fragments of ML at the GaLoP VII: Games for Logic and Programming Languages workshop in Dubrovnik

11/04/12. Gave a talk on Programs, Security and Games at the Science of Information Systems workshop, LIMS London

01/03/12. Organiser of the QMUL Theory Group Seminar. If you are interested in giving a seminar or being added to our mailing list, please contact me in the first instance