THE GUARDED LAMBDA-CALCULUS PROGRAMMING AND REASONING WITH GUARDED RECURSION FOR COINDUCTIVE TYPES
THE GUARDED LAMBDA-CALCULUS PROGRAMMING AND REASONING WITH GUARDED RECURSION FOR COINDUCTIVE TYPES
复制标题
DOI：
10.2168/lmcs-12(3:7)2016
复制
发表时间：
2016-01-01
影响因子：
0.6
通讯作者：
Birkedal, Lars
中科院分区：
文献类型：
--
作者：
Clouston, Ranald;Bizjak, Ales;Birkedal, Lars
我们提出了守卫的lambda-calculus，这是简单键入的lambda-calculus的扩展，并具有守卫的递归和共同感应类型。使用守卫的递归类型可确保计划良好的计划的生产力。受保护的递归类型可以通过受模态逻辑和ATKEY-MCBRIDE时钟定量启发的类型形式转换为共同感应类型，从而允许键入可抗性功能。我们为演算提供了逐个名称的操作语义，并在树木的拓扑中定义了足够的含义语义。适当的证明需要始终终止程序的评估。我们介绍了一个具有LOB归纳的程序逻辑，以推理程序的上下文等效性。我们通过显示解决方案的解决方案的确定性来证明积分的表现力。
We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive types may be transformed into coinductive types by a type-former inspired by modal logic and Atkey-McBride clock quantification, allowing the typing of acausal functions. We give a call-by-name operational semantics for the calculus, and define adequate denotational semantics in the topos of trees. The adequacy proof entails that the evaluation of a program always terminates. We introduce a program logic with Lob induction for reasoning about the contextual equivalence of programs. We demonstrate the expressiveness of the calculus by showing the definability of solutions to Rutten's behavioural differential equations.