Enumerating Well-Typed Terms Generically

被引：0

作者：

Yakushev, Alexey Rodriguez ^{[1
]}

Jeuring, Johan ^{[2
,3
]}

机构：

[1] Vector Fabr BV, Paradijslaan 28, NL-5611 KN Eindhoven, Netherlands

[2] Univ Utrecht, Dept Informat & Comp Sci, NL-3508 TB Utrecht, Netherlands

[3] Open Univ Netherlands, Sch Comp Sci, NL-6401 DL Heerlen, Netherlands

来源：

APPROACHES AND APPLICATIONS OF INDUCTIVE PROGRAMMING | 2010年 / 5812卷

关键词：

SCRAP;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We use generic programming techniques to generate well-typed lambda terms. We encode well-typed terms by means of generalized algebraic datatypes (GADTs) and existential types. The Spine approach to generic programming supports GADTs, but it does not support the definition of generic producers for existentials. We describe how to extend the Spine approach to support existentials and we use the improved Spine to define a generic enumeration function. We show that the enumeration function can be used to generate the terms of simply typed lambda calculus.

引用

页码：93 / +

页数：2

共 50 条

[21] Proof terms for simply typed higher order logic
Berghofer, S
Nipkow, T
THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 38 - 52
[22] Well-going programs can be typed
Kahrs, S
TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2003, 2701 : 167 - 179
[23] VeriML: Typed Computation of Logical Terms inside a Language with Effects
Stampoulis, Antonis
Shao, Zhong
ACM SIGPLAN NOTICES, 2010, 45 (09) : 333 - 344
[24] Typed lambda-terms in categorical attributed graph transformation
Boisvert, Bertrand
Feraud, Louis
Soloviev, Sergei
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (56): : 33 - 47
[25] VeriML: Typed Computation of Logical Terms inside a Language with Effects
Stampoulis, Antonis
Shao, Zhong
ICFP 2010: PROCEEDINGS OF THE 2010 ACM SIGPLAN INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING, 2010, : 333 - 344
[26] Boltzmann Samplers for Closed Simply-Typed Lambda Terms
Bendkowski, Maciej
Grygiel, Katarzyna
Tarau, Paul
PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES (PADL 2017), 2017, 10137 : 120 - 135
[27] ENUMERATING CERTAIN DESIGN PROBLEMS IN TERMS OF BI-COLORED GRAPHS WITH NO ISOLATES
HARARY, F
MARCH, L
ROBINSON, RW
ENVIRONMENT AND PLANNING B-PLANNING & DESIGN, 1978, 5 (01): : 31 - 43
[28] De Bruijn's syntax and reductional behaviour of λ-terms:: the typed case
Kamareddine, F
Bloo, R
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2005, 62 (02): : 159 - 189
[29] ARE CHEMICAL TERMS WELL DEFINED
HERRON, JD
JOURNAL OF CHEMICAL EDUCATION, 1977, 54 (12) : 758 - 758
[30] Compact Bit Encoding Schemes for Simply-Typed Lambda-Terms
Takeda, Kotaro
Kobayashi, Naoki
Yaguchi, Kazuya
Shinohara, Ayumi
ACM SIGPLAN NOTICES, 2016, 51 (09) : 146 - 157

← 1 2 3 4 5 →