Witnessing (Co)datatypes

被引：9

作者：

Blanchette, Jasmin Christian ^{[1
,2
,3
]}

Popescu, Andrei ^{[4
]}

Traytel, Dmitriy ^{[5
]}

机构：

[1] Inria Nancy, Villers Les Nancy, France

[2] LORIA, Villers Les Nancy, France

[3] Max Planck Inst Informat, D-66123 Saarbrucken, Germany

[4] Middlesex Univ, Sch Sci & Technol, Dept Comp Sci, London N17 8HR, England

[5] Tech Univ Munich, Fak Informat, D-80290 Munich, Germany

来源：

PROGRAMMING LANGUAGES AND SYSTEMS | 2015年 / 9032卷

关键词：

COINDUCTION; HOL;

D O I：

10.1007/978-3-662-46669-8_15

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

Datatypes and codatatypes are useful for specifying and reasoning about (possibly infinite) computational processes. The Isabelle/HOL proof assistant has recently been extended with a definitional package that supports both. We describe a complete procedure for deriving nonemptiness witnesses in the general mutually recursive, nested case-nonemptiness being a proviso for introducing types in higher-order logic.

引用

页码：359 / 382

页数：24

共 40 条

[1] Copatterns Programming Infinite Structures by Observations [J].

Abel, Andreas ;

Pientka, Brigitte ;

Thibodeau, David ;

Setzer, Anton .

ACM SIGPLAN NOTICES, 2013, 48 (01) :27-38

[2]

Adams M, 2010, LECT NOTES COMPUT SC, V6327, P142, DOI 10.1007/978-3-642-15582-6_25

[3]

[Anonymous], 2019, LCP ISABELLE 2019

[4]

[Anonymous], LECT NOTES COMPUTER

[5]

[Anonymous], 2011, LNCS

[6]

[Anonymous], 2011, P 26 ACM S APPL COMP

[7]

Arthan R. D., 2004, TPHOLS 2004 EMERGING, P1

[8] TERMINAL COALGEBRAS IN WELL-FOUNDED SET-THEORY [J].

BARR, M .

THEORETICAL COMPUTER SCIENCE, 1993, 114 (02) :299-315

[9]

Berghofer S, 1999, LECT NOTES COMPUT SC, V1690, P19

[10]

Bertot Y, 2005, LECT NOTES COMPUT SC, V3461, P102

← 1 2 3 4 →