Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
复制标题
高阶逻辑的基础（协同）数据类型和（协同）递归
DOI：
10.1007/978-3-319-66167-4_1
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Dmitriy Traytel
中科院分区：
文献类型：
--
作者：
Julian Biendarra;Jasmin Christian Blanchette;Aymeric Bouzy;Martin Desharnais;Mathias Fleury;Johannes Hölzl;Ondrej Kuncar;Andreas Lochbihler;Fabian Meier;Lorenz Panny;Andrei Popescu;Christian Sternagel;René Thiemann;Dmitriy Traytel
我们描述了2011年开始的一系列工作，目的是用协归纳数据类型丰富Isabelle/HOL的语言，这些数据类型允许无穷大的值，并且使用比以前任何基于高阶逻辑的系统所支持的更具表现力的归纳数据类型概念。这些(Co)数据类型由(Co)递归函数的定义原则和(Co)归纳的推理原则补充。与其他提供Codatatype的系统相比，我们的方法不需要额外的公理或逻辑扩展。
We describe a line of work that started in 2011 towards enriching Isabelle/HOL’s language with coinductive datatypes, which allow infinite values, and with a more expressive notion of inductive datatype than previously supported by any system based on higher-order logic. These (co)datatypes are complemented by definitional principles for (co)recursive functions and reasoning principles for (co)induction. In contrast with other systems offering codatatypes, no additional axioms or logic extensions are necessary with our approach.
登录
查看更多内容
为什么我们不能在 HOL 中使用 SML 风格的数据类型声明
DOI：
10.1016/b978-0-444-89880-7.50042-5
发表时间：
1992
期刊：
J. Log. Comput.
影响因子：
--
作者：
Elsa L. Gunter
通讯作者：
Elsa L. Gunter
抽象 GSOS 规则和递归定义的模块化处理
DOI：
10.2168/lmcs-9(3:28)2013
发表时间：
2013
期刊：
Log. Methods Comput. Sci.
影响因子：
--
作者：
Stefan Milius;L. Moss;D. Schwencke
通讯作者：
D. Schwencke
DOI：
10.1145/3009837.3009887
发表时间：
2016
期刊：
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
影响因子：
--
作者：
L. Kovács;Simon Robillard;A. Voronkov
通讯作者：
A. Voronkov
通过域和拓扑的惰性列表上的递归函数
DOI：
10.1007/978-3-319-08970-6_22
发表时间：
2014
期刊：
影响因子：
--
作者：
Andreas Lochbihler;Johannes Hölzl
通讯作者：
Johannes Hölzl
在 Isabelle/HOL 中查找终止证明的词典顺序
DOI：
--
发表时间：
2007
期刊：
International Conference on Theorem Proving in Higher Order Logics
影响因子：
--
作者：
Lukas Bulwahn;Alexander Krauss;T. Nipkow
通讯作者：
T. Nipkow