A cost-aware logical framework

We present \textbf{calf}, a \textbf{c}ost-\textbf{a}ware \textbf{l}ogical \textbf{f}ramework for studying quantitative aspects of functional programs. Taking inspiration from recent work that reconstructs traditional aspects of programming languages in terms of a modal account of \emph{phase distinctions}, we argue that the cost structure of programs motivates a phase distinction between \emph{intension} and \emph{extension}. Armed with this technology, we contribute a synthetic account of cost structure as a computational effect in which cost-aware programs enjoy an internal noninterference property: input/output behavior cannot depend on cost. As a full-spectrum dependent type theory, \textbf{calf} presents a unified language for programming and specification of both cost and behavior that can be integrated smoothly with existing mathematical libraries available in type theoretic proof assistants. We evaluate \textbf{calf} as a general framework for cost analysis by implementing two fundamental techniques for algorithm analysis: the \emph{method of recurrence relations} and \emph{physicist's method for amortized analysis}. We deploy these techniques on a variety of case studies: we prove a tight, closed bound for Euclid's algorithm, verify the amortized complexity of batched queues, and derive tight, closed bounds for the sequential and \emph{parallel} complexity of merge sort, all fully mechanized in the Agda proof assistant. Lastly we substantiate the soundness of quantitative reasoning in \textbf{calf} by means of a model construction.