@article{kavvos2025b,
author = {Kavvos, G. A.},
title = {Adequacy for Algebraic Effects Revisited},
year = {2025},
publisher = {Association for Computing Machinery},
volume = {9},
number = {OOPSLA1},
doi = {10.1145/3720457},
journal = {Proceedings of the ACM on Programming Languages},
articleno = {113},
}
@inproceedings{tune2026,
title = {Noninterference Through Bisimulation},
volume = {15652},
doi = {10.1007/978-3-031-99751-8_11},
series = {Lecture Notes in Computer Science},
pages = {259–280},
booktitle = {Trends in Functional Programming},
publisher = {Springer Nature Switzerland},
author = {Tune, April and Yang, Wendy and Kavvos, G. A.},
editor = {Gibbons, Jeremy},
date = {2026},
}
MFPS 2024
Two-dimensional Kripke Semantics II: Stability and Completeness
@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}
}
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
@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}
}
LMCS 2021
Multimodal Dependent Type Theory
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal
@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}
}
@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}
}
@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}
}