Decalf: A Directed, Effectful Cost-Aware Logical Framework [POPL 2024]

Code artifact associated with Decalf: A Directed, Effectful Cost-Aware Logical Framework.

@software{grodin-niu-sterling-harper:2024:agda,
  author = {Grodin, Harrison and Niu, Yue and Sterling, Jonathan and Harper, Robert},
  publisher = {GitHub},
  url = {https://github.com/jonsterling/agda-calf},
  year = {2024},
  title = {\texttt{agda-calf} v2.0.0},
  doi = {10.1145/3580425}
}

Amortized Analysis via Coinduction (Early Ideas) [CALCO 2023]

Formalization of Amortized Analysis via Coinduction (Early Ideas).

A Cost-Aware Logical Framework [POPL 2022]

Code artifact associated with A Cost-Aware Logical Framework.

@software{niu-sterling-grodin-harper:2022:agda,
  author = {Niu, Yue and Sterling, Jonathan and Grodin, Harrison and Harper, Robert},
  publisher = {GitHub},
  url = {https://github.com/jonsterling/agda-calf},
  year = {2022},
  title = {\texttt{agda-calf}},
  doi = {10.1145/3462303}
}