The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time. - G. A. Kavvos (CoRR, 2016)

On the Semantics of Intensionality. - G. A. Kavvos (FoSSaCS, 2017)

On the Semantics of Intensionality and Intensional Recursion. - G. A. Kavvos (CoRR, 2017)

On the semantics of intensionality and intensional recursion. - Georgios Alexandros Kavvos (2017)

Recurrence Extraction for Functional Programs through Call-by-Push-Value (Extended Version). - G. A. Kavvos; Edward Morehouse; Daniel R. Licata; Norman Danner (CoRR, 2019)

Modalities, cohesion, and information flow. - G. A. Kavvos (Proc. ACM Program. Lang., 2019)

Dual-Context Calculi for Modal Logic. - G. A. Kavvos (Log. Methods Comput. Sci., 2020)

Recurrence extraction for functional programs through call-by-push-value. - G. A. Kavvos; Edward Morehouse; Daniel R. Licata; Norman Danner (Proc. ACM Program. Lang., 2020)

Intensionality, Intensional Recursion and the Gödel-Löb Axiom. - G. A. Kavvos (FLAP, 2021)

Multimodal Dependent Type Theory. - Daniel Gratzer; G. A. Kavvos; Andreas Nuyts; Lars Birkedal (Log. Methods Comput. Sci., 2021)

Client-server sessions in linear logic. - Zesen Qian; G. A. Kavvos; Lars Birkedal (Proc. ACM Program. Lang., 2021)

Deeper Shallow Embeddings. - Jacob Prinz; G. A. Kavvos; Leonidas Lampropoulos (ITP, 2022)

Syllepsis in Homotopy Type Theory. - Kristina Sojakova; G. A. Kavvos (LICS, 2022)

Modalities and Parametric Adjoints. - Daniel Gratzer; Evan Cavallo; G. A. Kavvos; Adrien Guatto; Lars Birkedal (ACM Trans. Comput. Log., 2022)

Under Lock and Key: a Proof System for a Multimodal Logic. - G. A. Kavvos; Daniel Gratzer (Bull. Symb. Log., 2023)

Two-Dimensional Kripke Semantics I: Presheaves. - Georgios Alexandros Kavvos (FSCD, 2024)

Two-dimensional Kripke Semantics II: Stability and Completeness. - G. A. Kavvos (CoRR, 2024)

Adequacy for Algebraic Effects Revisited. - G. A. Kavvos (Proc. ACM Program. Lang., 2025)