This page lists the complete bibliography for the Cost-Aware Logical Framework (calf) project.
@article{niu-sterling-grodin-harper>2022,
title = {A cost-aware logical framework},
author = {Niu, Yue and Sterling, Jonathan and Grodin, Harrison and Harper, Robert},
year = {2022},
month = jan,
journal = {Proc. ACM Program. Lang.},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {6},
number = {POPL},
doi = {10.1145/3498670},
url = {https://doi.org/10.1145/3498670},
issue_date = {January 2022},
articleno = {9},
numpages = {31},
keywords = {algorithm analysis, amortized analysis, behavioral verification, cost models, equational reasoning, intensional property, mechanized proof, modal type theory, noninterference, parallel algorithms, phase distinction, proof assistants, recurrence relations}
}@article{grodin-niu-sterling-harper>2024,
title = {Decalf: A Directed, Effectful Cost-Aware Logical Framework},
author = {Grodin, Harrison and Niu, Yue and Sterling, Jonathan and Harper, Robert},
year = {2024},
month = jan,
journal = {Proc. ACM Program. Lang.},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {8},
number = {POPL},
doi = {10.1145/3632852},
url = {https://doi.org/10.1145/3632852},
issue_date = {January 2024},
articleno = {10},
numpages = {29},
keywords = {algorithm analysis, cost models, phase distinction, noninterference, intensional property, behavioral verification, equational reasoning, modal type theory, mechanized proof, proof assistants, recurrence relations, amortized analysis, parallel algorithms}
}@article{grodin-li-harper>2026,
title = {Abstraction Functions as Types: Modular Verification of Cost and Behavior in Dependent Type Theory},
author = {Grodin, Harrison and Li, Runming and Harper, Robert},
year = 2026,
month = jan,
journal = {Proc. ACM Program. Lang.},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = 10,
number = {POPL},
doi = {10.1145/3776673},
url = {https://doi.org/10.1145/3776673},
issue_date = {January 2026},
articleno = 31,
numpages = 28,
keywords = {abstract data type, abstraction, abstraction function, algorithm, algorithm analysis, call-by-push-value, concrete type, cost analysis, data structure, dependent type theory, equational reasoning, information flow, modal type theory, modularity, noninterference, phase distinction, verification}
}@phdthesis{niu>thesis,
title = {{Cost-sensitive programming, verification, and semantics}},
author = {Yue Niu},
year = {2025},
month = {2},
doi = {10.1184/R1/28352006.v1},
url = {https://kilthub.cmu.edu/articles/thesis/Cost-sensitive_programming_verification_and_semantics/28352006},
school = {Carnegie Mellon University}
}@misc{li-harper>2025,
title = {Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability},
author = {Runming Li and Robert Harper},
year = {2025},
url = {https://arxiv.org/abs/2504.12464},
eprint = {2504.12464},
archiveprefix = {arXiv},
primaryclass = {cs.PL}
}@inproceedings{li-yao-harper>2026,
title = {Mechanizing Synthetic Tait Computability in Istari},
author = {Li, Runming and Yao, Yue and Harper, Robert},
year = 2026,
booktitle = {Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs},
location = {Rennes, France},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
series = {CPP '26},
pages = {231–247},
doi = {10.1145/3779031.3779085},
isbn = 9798400723414,
url = {https://doi.org/10.1145/3779031.3779085},
numpages = 17,
keywords = {Istari, cost-aware logical framework, equality reflection, extensional type theory, gluing, logical relations, meta-theory, synthetic Tait computability}
}@inproceedings{grodin-harper>2023,
title = {{Amortized Analysis via Coinduction}},
author = {Grodin, Harrison and Harper, Robert},
year = {2023},
booktitle = {10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {270},
pages = {23:1--23:6},
doi = {10.4230/LIPIcs.CALCO.2023.23},
isbn = {978-3-95977-287-7},
issn = {1868-8969},
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.23},
editor = {Baldan, Paolo and de Paiva, Valeria},
urn = {urn:nbn:de:0030-drops-188201},
annote = {Keywords: amortized analysis, coinduction, data structure, mechanized proof}
}@article{grodin-harper>2024,
title = {Amortized Analysis via Coalgebra},
author = {Harrison Grodin and Robert Harper},
year = {2024},
month = {Dec},
journal = {Electronic Notes in Theoretical Informatics and Computer Science},
volume = {Volume 4 - Proceedings of MFPS XL},
doi = {10.46298/entics.14797},
issn = {2969-2431},
url = {https://entics.episciences.org/14797},
eid = {10},
keywords = {Computer Science - Programming Languages, Computer Science - Data Structures and Algorithms, Mathematics - Category Theory}
}@misc{li-grodin-harper>2023,
title = {A Verified Cost Analysis of Joinable Red-Black Trees},
author = {Runming Li and Harrison Grodin and Robert Harper},
year = {2023},
url = {https://arxiv.org/abs/2309.11056},
eprint = {2309.11056},
archiveprefix = {arXiv},
primaryclass = {cs.PL}
}@techreport{zhou>2025,
title = {Formally Verified Cost of the Parallel Prefix Sum Algorithm},
author = {Andrew Zhou},
year = {2025},
month = {aug},
url = {https://www.cs.cmu.edu/~runmingl/student/zhou-scan.pdf},
institution = {Carnegie Mellon University}
}@techreport{kebuladze>2025,
title = {Amortized Analysis of Splay Trees via a Lax Homomorphism},
author = {Lukas Kebuladze},
year = {2025},
month = {aug},
url = {https://www.cs.cmu.edu/~runmingl/student/kebuladze-splay.pdf},
institution = {Carnegie Mellon University}
}@inproceedings{niu-harper>2023,
title = {A Metalanguage for Cost-Aware Denotational Semantics},
author = {Niu, Yue and Harper, Robert},
year = {2023},
booktitle = {2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
pages = {1--14},
doi = {10.1109/LICS56636.2023.10175777},
keywords = {Computer languages;Analytical models;Costs;Computational modeling;Semantics;Programming;Calculus;types;semantics;cost analysis}
}@article{niu-sterling-harper>2024,
title = {Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory},
author = {Yue Niu and Jonathan Sterling and Robert Harper},
year = {2024},
month = {Dec},
journal = {Electronic Notes in Theoretical Informatics and Computer Science},
volume = {Volume 4 - Proceedings of MFPS XL},
doi = {10.46298/entics.14732},
issn = {2969-2431},
url = {https://entics.episciences.org/14732},
eid = {18},
keywords = {Computer Science - Programming Languages}
}