mrs*_*eve 7 haskell dependent-type isabelle
有基于高阶逻辑(HOL)的编程语言和定理证明器.例子包括Twelf,lambda prolog,Isabelle.例如,Twelf既是编程语言又是定理证明者,而Isabelle主要是一个定理证明者,但是对于Isabelle代码提取是可用的.
我正在寻找一种基于haskell的HOL编程语言.原因是我非常喜欢lambda prolog,但它并不是一种实用的编程语言.Lambda prolog缺少标准库,与外部库的接口似乎并不简单.问题是如果你需要一些功能,比如为文本文件编写解析器,你就不能与haskell的许多可用现有库接口,而且,没有标准库,所以你从头开始.
今天我遇到了Caledon编程语言,它似乎是作为硕士论文实现的.从github页面:
Caledon是一种依赖类型,多态,高阶逻辑编程语言.
这很有趣,因为它是用haskell编写的,所以它应该很容易扩展并与现有的haskell库接口.但似乎该项目处于初期阶段,我不确定是否实现了输入输出(IO).由于我今天才了解卡利多,我想我可能错过了一些其他项目.(顺便说一句,我对像prolog这样的标准逻辑编程语言不感兴趣).
除了Caledon之外,是否有基于高阶逻辑的编程语言在haskell中实现？
(我要求"在haskell中实现",因为它很容易连接可以提取到haskell或在haskell中实现的编程语言.例如,Agda编程语言可以编译为haskell代码,haskell库可以方便地使用如果你知道如何使用haskell库是非常容易的.我相信的许多其他编程语言(例如,ATS)只提供最小的公共分母,这是一个基于C的外部函数接口(FFI).在我看来,连接相当麻烦两个更高级的编程语言通过它们各自的基于C的FFI接口.因此,似乎是"它应该在haskell中实现"的一部分.此外,作为旁注,一些用户过去曾因为我将Agda描述为编程语言而投降,但当然这不是真的,即考虑库里 - 霍华德)