Decidable Logic in the Design of Functional Languages

被引：0
|
作者：
Huang, Hao [1 ]
Long, Huan [1 ]
机构：
[1] Shanghai Jiao Tong Univ, Dept Comp Sci, Shanghai 200030, Peoples R China
来源：
PROCEEDINGS OF 2012 2ND INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE AND NETWORK TECHNOLOGY (ICCSNT 2012) | 2012年
关键词：
typed lambda calculus; full abstraction; applicative bisimulation; Presburger Arithmetic;
D O I：
暂无
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
In this paper we present a call-by-value PCF that is a variant of typed lambda calculus with a decidable first order logic. The main motivation of this new call-by-value language is to verify the correctness and reliability of using decidable conditionals in the design of practical call-by-value functional languages. And another application of this new language is that it can be an intermediate language to compare expressiveness between functional languages after language design. We show that the new language has the least expressiveness as the original call-by-value PCF. The decidability of theoremhood in the new language can introduce dependent types to functional languages. A fully abstract encoding is given from original call-by-value PCF into the new language with respect to Abramsky's extended applicative bisimulation.
引用
收藏
页码：261 / 265
页数：5
相关论文
共 50 条
12345