Foundational extensible corecursion: a proof assistant perspective
Foundational extensible corecursion: a proof assistant perspective
复制标题
基础可扩展核心递归：证明助理的观点
DOI：
10.1145/2784731.2784732
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Dmitriy Traytel
中科院分区：
文献类型：
--
作者：
Jasmin Christian Blanchette;Andrei Popescu;Dmitriy Traytel
基于共递上限和关系参数，给出了一种安全定义共递函数的形式化框架。最终产品是一个通用的共递归，它允许在“友好”操作（包括构造函数）下进行共递归（甚至递归）调用。友好的共递归函数可以这样注册，从而增加了共递归的表达性。元理论在伊莎贝尔证明助手中形式化，构成了原型工具的核心。协递子由第一原理推导而来，不需要新的公理或逻辑的扩展。
This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to and relational parametricity. The end product is a general corecursor that allows corecursive (and even recursive) calls under "friendly" operations, including constructors. Friendly corecursive functions can be registered as such, thereby increasing the corecursor's expressiveness. The metatheory is formalized in the Isabelle proof assistant and forms the core of a prototype tool. The corecursor is derived from first principles, without requiring new axioms or extensions of the logic.
登录
查看更多内容
具有共同模式的有根据的递归：终止和生产力的统一方法
DOI：
--
发表时间：
2013
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
Andreas Abel;B. Pientka
通讯作者：
B. Pientka
影响因子：
0.6
作者：
Clouston, Ranald;Bizjak, Ales;Birkedal, Lars
通讯作者：
Birkedal, Lars
抽象 GSOS 规则和递归定义的模块化处理
DOI：
10.2168/lmcs-9(3:28)2013
发表时间：
2013
期刊：
Log. Methods Comput. Sci.
影响因子：
--
作者：
Stefan Milius;L. Moss;D. Schwencke
通讯作者：
D. Schwencke
归纳与递归
影响因子：
1.1
作者：
J. Storer
通讯作者：
J. Storer
影响因子：
0.5
作者：
J. Rutten
通讯作者：
J. Rutten