A cost-aware logical framework
A cost-aware logical framework
复制标题
成本意识逻辑框架
DOI：
10.1145/3498670
复制
发表时间：
2022
影响因子：
--
通讯作者：
Harper, Robert
中科院分区：
文献类型：
--
作者：
Niu, Yue;Sterling, Jonathan;Grodin, Harrison;Harper, Robert
我们提出了一个研究函数程序定量方面的成本意识逻辑框架。从最近的工作，重建传统方面的编程语言的模态帐户的阶段区别的灵感，我们认为，成本结构的程序激发了一个阶段之间的区别intensionandextension。有了这项技术，我们贡献了一个合成帐户的成本结构作为一个计算效果，其中成本意识的程序享有内部的不干扰属性：输入/输出行为不能依赖于成本。作为一个全谱依赖的类型理论，calf提出了一个统一的语言，编程和规范的成本和行为，可以顺利地集成与现有的数学图书馆提供的类型理论proof assistants.We评估calf作为一个通用框架的成本分析，实现两个基本技术的算法分析：themod的递归关系和物理学家的方法摊销分析。我们部署这些技术的各种案例研究：我们证明了一个紧密的，封闭的界限欧几里得的算法，验证分批队列的摊销复杂性，并推导出紧密的，封闭的界限顺序andparallelcomplexity合并排序，所有完全机械化的Agda证明助理。最后，通过一个模型的构造，证明了定量推理的合理性.
We presentcalf, acost-awarelogicalframework 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 ofphase distinctions, we argue that the cost structure of programs motivates a phase distinction betweenintensionandextension. 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,calfpresents 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 evaluatecalfas a general framework for cost analysis by implementing two fundamental techniques for algorithm analysis: themethod of recurrence relationsandphysicist’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 andparallelcomplexity of merge sort, all fully mechanized in the Agda proof assistant. Lastly we substantiate the soundness of quantitative reasoning incalfby means of a model construction.
登录
查看更多内容
DOI：
10.1137/0606031
发表时间：
1985-04
期刊：
Siam Journal on Algebraic and Discrete Methods
影响因子：
--
作者：
R. Tarjan
通讯作者：
R. Tarjan
PL/CV3的类型论
DOI：
10.1145/357233.357238
发表时间：
1984
期刊：
ACM Trans. Program. Lang. Syst.
影响因子：
--
作者：
R. Constable;Daniel R. Zlatin
通讯作者：
Daniel R. Zlatin
FIFO 队列的高效功能实现
DOI：
10.1016/0020-0190(82)90015-1
发表时间：
1982
期刊：
Inf. Process. Lett.
影响因子：
--
作者：
F. Burton
通讯作者：
F. Burton
类型论中部分可计算函数的计算复杂性和归纳
影响因子：
3.3
作者：
R. Constable;Karl Crary;W. Sieg;Richard Sommer;C. Talcott
通讯作者：
C. Talcott
同伦型理论的模态
DOI：
10.23638/lmcs-16(1:2)2020
发表时间：
2017
期刊：
Log. Methods Comput. Sci.
影响因子：
--
作者：
E. Rijke;Michael Shulman;Bas Spitters
通讯作者：
Bas Spitters