Computation in Refinement Logics for Type Theory

计算机科学关注的是建立抽象的结构， “信息空间”。 在其他领域有如此多的应用 因为这些结构是如此的普遍， 可以实现它们。 计算机科学家研究的法律，管理 信息处理，他们创造工具来帮助 构建结构，测试和理解它们的任务。 之间 迄今为止提供的最强大的工具是编程语言， 环境. 但该领域现在正在集中研究如何扩展这些 更强大和通用的工具，称为问题 解决环境。 这个建议是关于数学基础的 对于一类这样的系统。 这里所研究的系统类的特征在于它的关系 逻辑。 人们发现某种形式逻辑 为函数式编程语言和问题解决提供了基础。 解决环境。 这个想法是， 证明可以被解释为函数程序。 这个概念现在已经 已经研究了十多年，并在实践中得到了检验。 结果 鼓励了更深入的研究，因为编程方法 这些系统所建议的似乎比普通的更可靠 编程和更强大。 它能够利用结果 从定理证明、逻辑编程和严格编程 方法论 这项工作是关于如何把细节 这些元素在一起。 这一地区的发现可能会 极大地改变了人们编程和解决问题的方式， 某些精确的问题。 该地区目前是 英国、法国、瑞典、德国和美国的共同努力。 研究人员认为，很快这种正在测试的系统将被 广泛应用于计算机科学实验室之外。 本研究 解决了一些必须解决的核心理论问题 在那发生之前 它特别关注某些 这些系统可以由其用户增强的方式（反射） 以及解决问题的决定可以推迟的方法 在系统的目标导向解决问题的过程中（或 程序开发）。 延迟中心的想法 一种特殊的变量叫做逻辑变量。 调查结果将加深对 逻辑变量的各种使用与反射之间的关系 在计算机科学和逻辑的其他领域， 设计下一代的问题解决环境。

Computer science is concerned with building abstract structure in "information space". There are so many applications in other fields because these structures are so general and because computer hardware can realize them. Computer Scientist study the laws that govern the processing of information, and they create tools to assist in the task of building structures, testing and understanding them. Among the most powerful tools provided so far are programming languages and environments. But the field is now converging on ways to extend these environments to more powerful and general tools, called problem solving environments. This proposal is about the mathematical basis for one class of such system. The class of systems studied here is characterized by its relationship to logic. It has been discovered that a certain kind of formal logic provides a basis for both functional programming languages and problem solving environments. The idea is that constructive mathematical proofs can be interpreted as functional programs. This notion has now been studied for over a decade and tested in practice. Results have encouraged a much deeper study because the programming method suggested by these systems seems to be more reliable than ordinary programming and much more powerful. It is able to draw on results from theorem proving, logic programming and rigorous programming methodology. This work is concerned with details of how to bring these elements together. It is possible that the discoveries made in this area will significantly change the way people program and the way they solve certain kinds of precise problems. The area is currently the focus of a concerted effort in Britain, France, Sweden, Germany, and the U.S. Researchers feel that soon systems of the kind being tested will be widely used beyond the computer science laboratory. This research addresses some of the central theoretical problems that must be solved before that can happen. In particular it is concerned with certain ways that these systems can be augmented by their users (reflection) and with ways that decisions about solving a problem can be postponed in the process of systematic goal-directed problem-solving (or equivalently program development). The idea for postponement centers on the use of a special kind of variable called a logic variable. Results from this investigation will deepen understanding of the relationship between various uses of logic variables and reflection in other parts of computer science and logic and find use in the design of the next generation of problem solving environments.