# Alex Kavvos

Lecturer in Programming Languages

Department of Computer Science

University of Bristol

CV | ORCID | GScholar | Bristol Pure

*I am looking to recruit PhD students interested in any of the following themes.*

Research interests:

- programming languages (theory and semantics)
- type theory (in particular modal type theory)
- homotopy type theory
- logic (including modal and categorical logic)
- (higher) category theory
- formal models of computer security
- concurrency and process calculi

## Publications [bibtex]

G. A. Kavvos. “Dual-context calculi for modal logic”. To appear in

*Logical Methods in Computer Science*. Full version of LICS 2017 article. [arXiv]Daniel Gratzer et al. “Multimodal Dependent Type Theory”. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. New York, NY, USA: Association for Computing Machinery, 2020. [doi] [tech report].

G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner. “Recurrence Extraction for Functional Programs through Call-by-Push-Value”. In: Proceedings of the ACM on Programming Languages 4.POPL (2019). [arXiv (incl. proofs)] [doi] [slides]

G. A. Kavvos. “Modalities, Cohesion, and Information Flow”. In: Proceedings of the ACM on Programming Languages 3.POPL (2019). [arXiv] [doi] [slides]

G. A. Kavvos. “Intensionality, Intensional Recursion, and the Gödel-Löb axiom”. In: Proceedings of 7th Workshop on Intuitionistic Modal Logic and Applications (IMLA 2017). 2017. [arXiv] [slides]

G. A. Kavvos. “Dual-context calculi for modal logic”. In: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 2017. [doi] [preprint] [slides]

G. A. Kavvos. “On the Semantics of Intensionality”. In: Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS). ed. by Javier Esparza and Andrzej S. Murawski. Vol. 10203. Lecture Notes in Computer Science. Springer-Verlag Berlin Heidelberg, 2017. [doi] [arXiv] [slides]

## Pre-prints

G. A. Kavvos. “A Quantum of Direction”. Submitted to

*Mathematical Structures in Computer Science*. [local copy]G. A. Kavvos. “The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time”. 2016. [arXiv]

## Thesis

- G. A. Kavvos. “On the Semantics of Intensionality and Intensional Recursion.” Department of Computer Science, University of Oxford. 2017. [arXiv] [Oxford repository]

## Talks

*How to define things by recursion*. Logsem seminar, Department of Computer Science, Aarhus University. [slides]*Recurrence Extraction for Functional Programs.*Talk at the Athens Programming Language Seminar (27 Dec 2019). [slides]*Modalities, Cohesion, and Information Flow.*Talk at the MIT Categories Seminar, Massachusetts Institute of Technology (3 Dec 2018). [slides]*Curry-Howard for Modal Logic.*Invited seminar at the Graduate Center, City University of New York (30 Oct 2018). [slides]*A Type-Theoretic Alternative to LISP.*Talk at the 11th Panhellenic Logic Symposium (July 2017). [slides]*A Type-Theoretic Alternative to LISP.*Talk given at TYPES 2017. [slides]

## Misc. links

The Bristol Theory and Algorithms group website

The Bristol Programming Languages theme website

An entertaining comment about dependent types and people who work on them

The Panhellenic Logic Symposium website