Publications

@InProceedings{kavvos:LIPIcs.FSCD.2024.14,
  author =	{Kavvos, G. A.},
  title =	{{Two-Dimensional Kripke Semantics I: Presheaves}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{14:1--14:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  doi =		{10.4230/LIPIcs.FSCD.2024.14},
}

@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},
}

@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}
}

@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},
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}

@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}
}