A cost-aware logical framework
Abstract
We present calf , a c ost- a ware l ogical 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 phase distinctions , we argue that the cost structure of programs motivates a phase distinction between intension and 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, 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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 12, 2022
- Source ID
- 10.1145/3498670
Entities
People
- Harrison Grodin
- Jonathan Sterling
- Robert Harper
- Yue Niu
Organizations
- Aarhus University
- Air Force Office of Scientific Research
- Air Force Research Laboratory
- Carnegie Mellon University
- National Science Foundation