Combining Proofs and Programs
Combining Proofs and Programs
复制标题
结合证明和程序
DOI：
10.4230/lipics.rta.2011.9
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Stephanie Weirich
中科院分区：
文献类型：
--
作者：
Stephanie Weirich
基于依赖类型理论的编程语言有两个巨大的进步：灵活性和安全性。通过依赖类型提供的类型级计算，算法可以更加通用，因为类型系统可以通过编程来表达灵活的接口。同样，类型级计算也可以表示数据结构不变量，这样程序就可以通过类型检查来证明正确性。此外，尽管有这些扩展，程序员已经知道了一切。通过Curry-Howard同构，类型级计算和验证逻辑的语言就是编程语言本身。
目前有两种设计依赖类型语言的方法：Coq，Epigram，Agda，它们源于证明助手的逻辑，要求所有表达式都终止。这些语言提供了可判定的类型检查和强大的正确性保证。相比之下，函数式编程语言，如Haskell和Omega，已经适应了特征依赖类型理论，但保留了类型和程序之间的严格划分。这些语言用终止义务换取更有限的正确性保证。
在这次演讲中，我将介绍Trellys项目的一个正在进行的概述。Trellys是一种新的核心语言，旨在提供从函数式编程到依赖类型编程的平滑路径。与传统的依赖类型理论和函数式语言不同，Trellys允许程序员统一使用全函数和部分函数。语言本身由两个片段组成，它们共享一个共同的语法和重叠的语义：一个简单的逻辑语言，保证完全正确性，一个表达性的按值调用编程语言，保证类型安全但不终止。
重要的是，这两个片段相互作用。逻辑片段可以充分地推理出有效的、局部的功能。程序值可以被逻辑用作证据。我们称这个原则为言论自由：尽管证明本身必须终止，但必须允许它们对程序员可能编写的任何函数进行推理。为了保持一致性，Trellys类型系统跟踪潜在的非终止计算可能出现的位置，以便它可以防止它们被用作证明。
Programming languages based on dependent type theory promise two great advances: flexibility and security. With the type-level computation afforded by dependent types, algorithms can be more generic, as the type system can express flexible interfaces via programming. Likewise, type-level computation can also express data structure invariants, so that programs can be proved correct through type checking. Furthermore, despite these extensions, programmers already know everything. Via the Curry-Howard isomorphism, the language of type-level computation and the verification logic is the programming language itself.
There are two current approaches to the design of dependently-typed languages: Coq, Epigram, Agda, which grew out of the logics of proof assistants, require that all expressions terminate. These languages provide decidable type checking and strong correctness guarantees. In contrast, functional programming languages, like Haskell and Omega, have adapted the features dependent type theories, but retain a strict division between types and programs. These languages trade termination obligations for more limited correctness assurances.
In this talk, I present a work-in-progress overview of the Trellys project. Trellys is new core language, designed to provide a smooth path from functional programming to dependently-typed programming. Unlike traditional dependent type theories and functional languages, Trellys allows programmers to work with total and partial functions uniformly. The language itself is composed of two fragments that share a common syntax and overlapping semantics: a simple logical language that guarantees total correctness and an expressive call-by-value programming language that guarantees types safety but not termination.
Importantly, these two fragments interact. The logical fragment may soundly reason about effectful, partial functions. Program values may be used as evidence by the logic. We call this principle freedom of speech: whereas proofs themselves must terminate, they must be allowed to reason about any function a programmer might write. To retain consistency, the Trellys type system keeps track of where potentially non-terminating computations may appear, so that it can prevent them from being used as proofs.
构造正确并发性：使用依赖类型来验证有效资源使用协议的实现
影响因子：
0.8
作者：
Brady E
通讯作者：
Brady E
总解析器组合器
影响因子：
--
作者：
Danielsson N
通讯作者：
Danielsson N