Centre for Metacomputation

元计算涉及用于分析程序行为的复杂计算工具的开发。这些工具可以在开发时运行，例如捕获错误，或者它们可以在运行时运行，例如使程序适应不断变化的工作负载。元计算的技术来自不同的领域，包括逻辑、自动定理证明、编译器构造、程序分析和软件工程。将这些分散的努力统一到不同的社区，并帮助建立新兴的元计算领域及其基础的时机已经成熟。这样做是这项提议的主要目的。这些不同技术之间的协同作用取得了惊人的实践成功的例子比比皆是。微软的SLAM项目结合了自动定理证明(模型检查和演绎证明)以及程序分析的技术，以定位设备驱动程序中的任何故障。由IBM开发的Eclipse重构工具使用复杂的类型约束系统来正确实现重构转换，如提取接口。英特尔的Forte框架使用了一种具有反射和元编程功能的函数式编程语言，为验证工业规模的硬件设计提供了一个有效的框架。语义学的基础工作现在已经达到了可以将语义视为一种简单的程序分析数学工具，而是直接导致计算表示和算法方法的地步。模型检查已经可以被视为朝这个方向迈出的一步。然而，我们看到了在这种情况下使用组合语义方法的巨大潜力；特别是在开放系统的分析中。被赋予计算方面的语义学本质上是元计算的，出现了许多有趣的新问题和可能性。一方面，可以设想在程序分析中有一些新的和非常直接的应用。围绕反射也有一些有趣的问题：一个程序能否成为其自身语义的计算表示，这种反身性是否有用？更广泛地说，我们认为语义和程序分析社区之间的协同作用越来越大，这对两者都有很大的好处，在程序分析中提供了更深的深度和形式上的严谨性，以及语义中的计算方面的新挑战和链接。

Metacomputation concerns the development of sophisticatedcomputational tools for analysing the behaviour of programs. Suchtools may operate at development time, for example to catch bugs, orthey may operate at run-time, for instance to adapt the program tochanging workloads. Techniques in metacomputation draw from a broadvariety of different fields, including logic, automated theoremproving, compiler construction, program analysis, and softwareengineering. The time is ripe to unify these fragmented efforts indifferent communities and to help establish the emerging field ofmetacomputation and its foundations. To do so is the primary objectiveof this proposal.Examples abound where synergy between these different techniques hasled to striking practical success. The SLAM project at Microsoftcombines techniques from automated theorem proving (both modelchecking and deductive proof) as well as program analysis to locatemany faults in device drivers. The Eclipse refactoring tools,developed at IBM, use a sophisticated system of type constraints tocorrectly implement refactoring transformations such as extractinterface. Intel's Forte framework employs a functional programminglanguage with reflection and metaprogramming features to get aneffective framework for verification of industrial-scale hardwaredesigns.Foundational work in semantics has now reached a point where semanticscan be seen, not simply as a mathematical tool for the analysis ofprograms, but as leading directly to computational representations andalgorithmic methods. Model-checking can already be seen as a step inthis direction. However, we see great additional potential in the useof compositional semantic methods in this context; in particular, inthe analysis of open systems. Semantics endowed with a computationalaspect is inherently metacomputational in nature, and many interestingnew questions and possibilities arise. One the one hand, some new andvery direct applications in program analysis can be envisaged. Thereare also some fascinating issues around reflection: can a program bethe computational representation of its own semantics, and can suchreflexivity be useful?More broadly, we see a growing synergy between the semantics andprogram analysis community as greatly to the benefit of both,providing increased depth and formal rigour in program analysis, andnew challenges and links to computational aspects in semantics.