Publications

Pre-prints

2024
Two-dimensional Kripke Semantics II: Completeness and Stability
G. A. Kavvos
2024
Two-dimensional Kripke Semantics
G. A. Kavvos
2019
A Quantum of Direction
G. A. Kavvos

Papers

BSL 2023
Under Lock and Key: A Proof System for a Multimodal Logic
G. A. Kavvos and Daniel Gratzer
@article{kavvos2023,
  title = {Under Lock and Key: A Proof System for a Multimodal Logic},
  volume = {29},
  doi = {10.1017/bsl.2023.14},
  pages = {264--293},
  number = {2},
  journaltitle = {The Bulletin of Symbolic Logic},
  author = {Kavvos, G. A. and Gratzer, Daniel},
  date = {2023},
}

LICS 2022
Syllepsis in Homotopy Type Theory
Kristina Sojakova and G. A. Kavvos
@inproceedings{sojakova2022,
  author = {Sojakova, Kristina and Kavvos, G. A.},
  title = {Syllepsis in Homotopy Type Theory},
  year = {2022},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/3531130.3533347},
  booktitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science},
  articleno = {29}
}

ITP 2022
Deeper Shallow Embeddings
Jacob Prinz, G. A. Kavvos, and Leonidas Lampropoulos
@InProceedings{prinz2022,
  author =	{Prinz, Jacob and Kavvos, G. A. and Lampropoulos, Leonidas},
  title =	{{Deeper Shallow Embeddings}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{28:1--28:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  doi =		{10.4230/LIPIcs.ITP.2022.28},
}

TOCL 2022
Modalities and Parametric Adjoints
Daniel Gratzer, Evan Cavallo, G. A. Kavvos, Adrien Guatto, and Lars Birkedal
@article{gratzer2022a,
  author = {Gratzer, Daniel and Cavallo, Evan and Kavvos, G. A. and Guatto, Adrien and Birkedal, Lars},
  title = {Modalities and {P}arametric {A}djoints},
  year = {2022},
  publisher = {Association for Computing Machinery},
  volume = {23},
  number = {3},
  doi = {10.1145/3514241},
  journal = {ACM Transactions on Computational Logic},
  articleno = {18},
  numpages = {29}
}

IfCoLog 2021
Intensionality, Intensional Recursion, and the Gödel–Löb Axiom
G. A. Kavvos
Originally presented at IMLA 2017.
@article{kavvos2021,
  author = {Kavvos, G. A.},
  title = {Intensionality, Intensional Recursion, and the {G}\"{o}del-{L}\"{o}b Axiom},
  year = {2021},
  journal = {Journal of Applied Logics - The IfCoLog Journal of Logics and their Applications},
  volume = {8},
  issue = {8},
  pages = {2287-2311},
  eprinttype = {arxiv},
  eprint = {1703.01288}
}

ICFP 2021
Client-Server Sessions in Linear Logic
Zesen Qian, G. A. Kavvos, and Lars Birkedal
Distinguished paper award.
@article{qian2021,
  author = {Qian, Zesen and Kavvos, G. A. and Birkedal, Lars},
  title = {Client-Server Sessions in Linear Logic},
  year = {2021},
  publisher = {Association for Computing Machinery},
  journal = {Proceedings of the ACM on Programming Languages},
  address = {New York, NY, USA},
  volume = {5},
  number = {ICFP},
  doi = {10.1145/3473567},
  articleno = {62},
  numpages = {31}
}

LMCS 2021
Multimodal Dependent Type Theory
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal
Full version of LICS 2020 article.
@article{gratzer2021,
  title = {Multimodal Dependent Type Theory},
  author = {Daniel Gratzer and G. A. Kavvos and Andreas Nuyts and Lars Birkedal},
  doi = {10.46298/lmcs-17(3:11)2021},
  journal = {{Logical Methods in Computer Science}},
  volume = {17},
  issue = {3},
  year = {2021}
}

LMCS 2020
Dual-Context Calculi for Modal Logic
G. A. Kavvos
Full version of LICS 2017 article.
@article{kavvos2020,
  title = {Dual-Context Calculi for Modal Logic},
  author = {Kavvos, G. A.},
  journal = {Logical Methods in Computer Science},
  year = {2020},
  volume = {16},
  issue = {3},
  doi = {10.23638/LMCS-16(3:10)2020}
}

LICS 2020
Multimodal Dependent Type Theory
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal
@inproceedings{gratzer2020,
  author = {Gratzer, Daniel and Kavvos, G. A. and Nuyts, Andreas and Birkedal, Lars},
  title = {Multimodal Dependent Type Theory},
  year = {2020},
  isbn = {9781450371049},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/3373718.3394736},
  booktitle = {Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science},
  pages = {492–506},
  numpages = {15}
}

POPL 2020
Recurrence Extraction for Functional Programs through Call-by-Push-Value
G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner
@article{kavvos2019b,
  author = {Kavvos, G. A. and Morehouse, Edward and Licata, Daniel R. and Danner, Norman},
  title = {Recurrence Extraction for Functional Programs through Call-by-Push-Value},
  year = {2019},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {4},
  issue = {POPL},
  doi = {10.1145/3371083},
  journal = {Proceedings of the ACM on Programming Languages},
  articleno = {15},
  numpages = {31},
  eprinttype = {arxiv},
  eprint = {1911.04588}
}

POPL 2019
Modalities, Cohesion, and Information Flow
G. A. Kavvos
@article{kavvos2019a,
  author = {Kavvos, G. A.},
  title = {Modalities, Cohesion, and Information Flow},
  year = {2019},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {3},
  issue = {POPL},
  doi = {10.1145/3290333},
  journal = {Proceedings of the ACM on Programming Languages},
  articleno = {20},
  numpages = {29}
}

LICS 2017
Dual-context calculi for modal logic
G. A. Kavvos
@inproceedings{kavvos2017b,
  title = {Dual-context calculi for modal logic},
  author = {Kavvos, G. A.},
  doi = {10.1109/LICS.2017.8005089},
  isbn = {978-1-5090-3018-7},
  booktitle = {2017 32nd {Annual} {ACM}/{IEEE} {Symposium} on {Logic} in {Computer} {Science} ({LICS})},
  publisher = {IEEE},
  year = {2017}
}

FoSSaCS 2017
On the Semantics of Intensionality
G. A. Kavvos
@inproceedings{kavvos2017a,
  title = {On the {Semantics} of {Intensionality}},
  isbn = {978-3-662-54458-7},
  series = {Lecture {Notes} in {Computer} {Science}},
  volume = {10203},
  doi = {10.1007/978-3-662-54458-7_32},
  booktitle = {Foundations of {Software} {Science} and {Computation} {Structures}},
  publisher = {Springer Berlin Heidelberg},
  author = {Kavvos, G. A.},
  editor = {Esparza, Javier and Murawski, Andrzej S.},
  year = {2017},
  pages = {550--566},
  eprinttype = {arxiv},
  eprint = {1602.01365}
}