US-France (INRIA) Cooperative Research: Type Theory and Interactive Development of Proofs and Programs

该奖项将支持宾夕法尼亚大学、斯坦福大学和康奈尔大学的研究人员与法国国家信息科学与自动化研究所（INRIA）和巴黎高等师范学院合作开展的计算机科学小组研究工作。美国小组将由宾夕法尼亚大学的卡尔·冈特博士和瓦尔·布雷祖-坦宁博士领导。在法国方面，该项目将由罗昆古研究所的Thierry Coquand博士领导。为期三年的联合访问和研讨会将重点关注类型系统的理论和应用。这组美国研究人员和他们的法国同行在程序设计理论、逻辑和代数之间的界面上取得了重要的成果。研究人员目前正在见证逻辑、数学和计算机科学之间的融合，例如，类型、证明和程序之间的深层联系正在被发现。然而，仍有许多工作要做，预计会发现进一步的联系和相似之处。正如在任何其他快速发展的领域一样，许多可供选择的系统和模型正在被研究，它们之间的相互关系只是部分被理解。在这一领域，美国和法国一些最重要的研究人员之间加强合作，可能会在这些替代方案的分类和统一方面取得重要成果。改进的语义模型支持参数多态性和类型继承的组合，这对于开发语义上更一致的面向对象编程语言是特别有意义的，这无疑是软件工程师感兴趣的问题。在另一个领域，美国在高阶逻辑编程方面的工作与法国在基于逻辑的语言定义系统方面的工作之间的互动有望非常富有成效，并为程序验证和语言定义系统带来更好的原型环境。

This award will support a group research effort in computer science to be carried out by researchers based at the University of Pennsylvania, Stanford University and Cornell University in collaboration with the French National Institute for Information Science and Automation (INRIA) and the Ecole Normale Superieure, Paris. The U.S. group will be led by Dr. Carl Gunter and Dr. Val Breazu-Tannen, University of Pennsylvania. On the French side the project will be led by Dr. Thierry Coquand, INRIA Rocquencourt. The three year program of joint visits and workshops will focus on the theory and applications of type systems. This group of U.S. researchers and their French counterparts have produced important results at the interface between the theory of programming, logic and algebra. Researchers are presently witnessing a convergence between logic, mathematics and computer science, in which, for example, deep connections between types, proofs and programs are being discovered. However, much remains to be done and discoveries of further connections and parallels are anticipated. As in any other rapidly advancing field, many alternative systems and models are being investigated, whose interrelationships are only partly understood. Improved collaboration between some of the foremost U.S. and French researchers in this area is likely to lead to important results in the classification and unification of those alternatives. Improved semantic models supporting the combination of parametric polymorphism and type inheritance would be of particular interest to the development of semantically more coherent object-oriented programming languages, a question of undoubted interest for software engineers. In a different area, the interaction between U.S. work on higher-order logic programming and French work on logic-based language definition systems promises to be very productive and lead to better prototyping environments for program-proving and language-definition systems.