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 (2020). “Dual-Context Calculi for Modal Logic”. In: Logical Methods in Computer Science 16 (3). [link]
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal. “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. [link] [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). [link] [slides]
G. A. Kavvos. “Modalities, Cohesion, and Information Flow”. In: Proceedings of the ACM on Programming Languages 3.POPL (2019). [link] [slides]
G. A. Kavvos. “Intensionality, Intensional Recursion, and the Gödel-Löb axiom”. To appear in the 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. [link] [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. [link] [slides]
Pre-prints
Zesen Qian, G. A. Kavvos, and Lars Birkedal. “Client-Server Sessions in Linear Logic”. 2020. [arXiv]
G. A. Kavvos. “A Quantum of Direction”. 2019. [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 PLS Lab.
The Bristol Programming Languages group website
An entertaining comment about dependent types and people who work on them
The Panhellenic Logic Symposium website