4 papers · 1 filter
Amortized Analysis via Coalgebra
Harrison Grodin, Robert Harper
Amortized analysis is a cost analysis technique for data structures in which cost is studied in aggregate: rather than considering the maximum cost of a single operation, one bound…
A Verified Cost Analysis of Joinable Red-Black Trees
Runming Li, Harrison Grodin, Robert Harper
Ordered sequences of data, specified with a join operation to combine sequences, serve as a foundation for the implementation of parallel functional algorithms. This abstract data…
Decalf: A Directed, Effectful Cost-Aware Logical Framework
Harrison Grodin, Yue Niu, Jonathan Sterling +1
We present Decalf, a directed, effectful cost-aware logical framework for studying quantitative aspects of functional programs with effects. Like Calf, the language is based on an…
A cost-aware logical framework
Yue Niu, Jonathan Sterling, Harrison Grodin +1
We present , a ost-ware ogical ramework for studying quantitative aspects of functional programs. Taking inspiration…