This program is tentative and subject to change.

Fri 21 Jan 2022 15:05 - 15:30 at Salon III - Type Theory Chair(s): Kuen-Bang Hou (Favonia)

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.

This program is tentative and subject to change.

Fri 21 Jan

Displayed time zone: Eastern Time (US & Canada) change

15:05 - 16:20
Type TheoryPOPL at Salon III
Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota, Twin Cities
15:05
25m
Research paper
A cost-aware logical frameworkInPerson
POPL
Yue Niu Carnegie Mellon University, Jonathan Sterling Aarhus University, Denmark, Harrison Grodin Carnegie Mellon University, Robert Harper Carnegie Mellon University, USA
Pre-print Media Attached
15:30
25m
Research paper
Formal Metatheory of Second-Order Abstract SyntaxDistinguished PaperRemote
POPL
Marcelo Fiore Computer Laboratory, University of Cambridge, Dmitrij Szamozvancev University of Cambridge
15:55
25m
Research paper
Observational Equality: Now For GoodDistinguished PaperRemote
POPL
Loïc Pujet Gallinette Project-Team, Inria, Nicolas Tabareau Inria
Hide past events