Focusing and Higher-Order Abstract Syntax

被引：20
作者：
Zeilberger, Noam [1 ]
机构：
[1] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA
来源：
POPL'08: PROCEEDINGS OF THE 35TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES | 2008年
关键词：
D O I：
10.1145/1328438.1328482
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
引用
收藏
页码：359 / 369
页数：11
相关论文
共 26 条
[1]  
Abadi M., 1991, Journal of Functional Programming, V1, P375, DOI 10.1017/S0956796800000186
[2]  
Andreoli J. M., 1992, Journal of Logic and Computation, V2, P297, DOI 10.1093/logcom/2.3.297
[3]   Focussing and proof construction [J].
Andreoli, JM .
ANNALS OF PURE AND APPLIED LOGIC, 2001, 107 (1-3) :131-163
[4]  
BRANDT M, 1998, FUNDAMENTA INFORM, V20, P1
[5]  
Buchholz W., 1981, Iterated Inductive Definitions and Subsystems of Analysis
[6]   Pattern matching as cut elimination [J].
Cerrito, S ;
Kesner, D .
THEORETICAL COMPUTER SCIENCE, 2004, 323 (1-3) :71-127
[7]  
*COQ DEV TEAM, 2006, COQ PROOF ASS REF MA
[8]   THE CALCULUS OF CONSTRUCTIONS [J].
COQUAND, T ;
HUET, G .
INFORMATION AND COMPUTATION, 1988, 76 (2-3) :95-120
[9]  
COQUAND T, 1992, P WORKSH TYP PROOFS, P71
[10]  
COQUAND T, 1989, LNCS, V389
123