# Alex Kavvos

Department of Computer Science

Aarhus University

Åbogade 34

8200 Aarhus N

Denmark

CV | ORCID | GScholar | Aarhus

*Starting in July 2020 I will be a Lecturer in Programming Languages at the University of Bristol*

Research interests:

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

## Publications

Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal. “Multimodal Dependent Type Theory”. To appear in: Proceedings of LICS 2020. [preprint] [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 (2020). [arXiv (w/ 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] [arXiv] [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, pp. 550–566. [doi] [arXiv]

## Pre-prints

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

*Mathematical Structures in Computer Science*. [local copy]G. A. Kavvos. “Dual-context calculi for modal logic”. Full version of LICS 2017 paper, submitted to

*Logical Methods in Computer Science*. [arXiv] [technical report]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.

COMP 115, How to Design Programs (Wesleyan, Spring 2019)

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

A link to the Panhellenic Logic Symposium