Higher-Order Abstract Syntax in Coq

TLCA, pp. 124-138, 1995.

被引用141|引用|浏览0|
EI
其它链接dl.acm.org|dblp.uni-trier.de|academic.microsoft.com
关键词
higher-order abstract syntaxsecond ordertyped lambda calculusprogramming languagenatural deduction

摘要

The terms of the simply-typed lambda-calculus can be used to express the higher-order abstract syntax of objects such as logical formulas, proofs, and programs. Support for the manipulation of such objects is provided in several programming languages (e.g. lambdaProlog, Elf). Such languages also provide embedded implication, a tool which...更多

代码

数据

PDF 全文
您的评分 :
0

 

标签
评论