Special Projects: Proofs as Programs

俄勒冈大学尤金分校已得到支持，将举办一个暑期班，讨论日益重要的“证明即计划”模式。根据这个范例，一个类型断言M：A有几个“同构”的解释。在计算解释中，M是(函数)程序，类型A是它的规范。在逻辑解释中，M是命题A的证明。这两种解释之间的联系的发现要归功于库里、霍华德和德布鲁因。50年后，证明和程序之间的这种联系现在被确立为许多关于程序的正式系统和自动化推理技术的基础。该学院的目标是培养感兴趣的研究生、学者和软件工程师在该领域进行研究。课程将包括为所有与会者提供的基本基础材料；为对新研究方向感兴趣的人提供的高级材料；为对实际应用感兴趣的人提供的各种工具的回顾以及使用这些工具完成各种任务的经验。更详细地说，课程将包括以下三大类讲座：1.背景：这份材料由80年代末和90年代初S和90年代初发展的成熟成果组成。这一背景信息将提供对该范式的基本概念和方法的介绍。高级主题：本材料包含更新的结果，这些结果是对早期工作的扩展和概括。这将为学生提供对研究和开放问题的洞察力。应用：这份材料将展示理论结果如何被计算机科学各个领域的从业者使用。这将为学生提供使用正式方法来推理和生成实际问题的解决方案的技能，例如硬件协议和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.