Special Projects: Proofs as Programs

EIA-0214927 Ariola，ZenaUniversity of Oregon特别项目：证明即方案尤金的俄勒冈州大学得到了支持，组织了一个关于证明即方案这一日益重要的范例的暑期学校。根据这个范例，一个类型化断言M：A有几个“同构”的解释。在计算解释中，M是一个（函数）程序，类型A是它的规格说明。在逻辑解释中，M是命题A的证明。发现这两种解释之间的联系是由于咖喱、霍华德和德布鲁因。五十年后，证明和程序之间的这种联系现已建立，成为许多正式系统和程序推理自动化技术的基础。学校的目标是为感兴趣的研究生、学者和软件工程师进行研究做好准备该领域。该课程将包括所有与会者的基本基础材料;对新的研究方向感兴趣的人的高级材料;以及对各种工具的回顾，以及对实际应用感兴趣的人将其用于各种任务的经验。更详细地说，课程将包括以下三个主要类别的讲座：1。背景：该材料由80年代末和90年代初开发的成熟结果组成。这些背景信息将提供一个基本概念和方法的范例的介绍。高级主题：本材料由最近的结果组成，这些结果扩展和推广了早期的工作。这将为学生提供对研究和开放问题的见解。3.应用：本材料将展示理论结果如何被计算机科学各个领域的从业者使用。这将为学生提供使用正式方法来推理和生成实际问题的解决方案的技能，例如硬件协议和Java规范的验证。

EIA-0214927Ariola, ZenaUniversity of OregonSpecial Projects: Proofs as ProgramsThe University of Oregon at Eugene has been provided with support to organize a summer school on the increasingly important paradigm of proofs-as-programs. According to this paradigm a typing assertion M: A has several "isomorphic" interpretations. In the computational interpretation, M is a (functional) program and the type A is its specification. In the logical interpretation M is a proof of the proposition A. The discovery of the connection between the two interpretations is due to Curry, Howard, and DeBruijn. Fifty years later, this connection between proofs and programs is now established as the foundation of many formal systems and automated techniques for reasoning about programs.The aim of the school is to prepare interested graduate students, academics, and software engineers for conducting research in the area. The curriculum will include basic foundational material for all attendees; advanced material for those interested in new research directions; and a review of various tools together with experience in using them for various tasks for those interested in practical applications. In more detail, the curriculum will include the following three major categories of lectures:1. Background: This material consists of well-established results developed in the late 80's and early 90's. This background information will provide an introduction to the essential concepts and methodologies of the paradigm.2. Advanced Topics: This material consists of more recent results that extend and generalize the earlier work. This will provide students with insights into research and open questions.3. Applications: This material will demonstrate how theoretical results can be used by practitioners in various fields of computer science. This will provide students with skills in the use of formal methods to reason about and generate solutions to practical problems, such as verification of hardware protocols and Java specifications.