Centre for Metacomputation

元计算中心

• 批准号: EP/D037085/1
• 负责人: Samson Abramsky
• 金额: $ 54.93万
• 依托单位: University of Oxford
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2006
• 资助国家: 英国
• 起止时间: 2006 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FD037085%2F1
• 关键词: Centre; Metacomputation

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.

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

项目成果

Automatic Abstraction in Symbolic Trajectory Evaluation

• DOI: 10.1109/famcad.2007.27
• 发表时间: 2007-11
• 期刊: Formal Methods in Computer Aided Design (FMCAD'07)
• 作者: Sara Adams;Magnus Björk;T. Melham;C. Seger

Tools and Algorithms for the Construction and Analysis of Systems

用于系统构建和分析的工具和算法

• DOI: 10.1007/978-3-642-28756-5_47
• 发表时间: 2012
• 作者: Basler G

Coalgebraic analysis of subgame-perfect equilibria in infinite games without discounting

无折扣无限博弈中子博弈完美均衡的代数分析

• DOI: 10.1017/s0960129515000365
• 发表时间: 2015
• 期刊: Mathematical Structures in Computer Science
• 影响因子: 0.5
• 作者: ABRAMSKY S

Termination analysis and call graph construction for higher-order functional programs

高阶函数程序的终止分析和调用图构建

• DOI: 10.1145/1291220.1291165
• 发表时间: 2007
• 期刊: ACM SIGPLAN Notices
• 作者: Sereni D