arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 1009.2189cs.LOcs.PL
收藏

第五届逻辑框架和元语言国际研讨会:理论与实践

Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice

Karl Crary, Marino Miculan

摘要:

类型论、逻辑框架和元语言构成了设计、实现和推理形式语言及其语义的共同基础。它们是现代程序设计语言、认证软件和特定领域逻辑设计的核心。更广泛地说,它们继续影响着数学、逻辑和计算机科学许多领域的应用。逻辑框架和元语言:理论与实践研讨会旨在汇集设计师,实施者和从业者在这些领域的工作,特别是关于:自动化和实施的元理论的程序设计语言和相关演算;设计证明助手,自动定理证明器,和正式的数字图书馆建立在逻辑框架技术;关于变量绑定和新名称生成的编码的理论和实践问题,特别是从绑定签名定义的数据集的表示和推理;元编程的案例研究,以及程序设计语言和其他演算的描述的(Meta)理论的机械化。本卷包含2010年7月14日在爱丁堡(英国)举行的LFMTP 2010上提交的论文的最终版本和修订版本。LFMTP 2010是联邦逻辑会议(FLoC 2010)的一部分,并与LICS 2010相关联。

英文摘要:

Type theories, logical frameworks and meta-languages form a common foundation for designing, implementing, and reasoning about formal languages and their semantics. They are central to the design of modern programming languages, certified software, and domain specific logics. More generally, they continue to influence applications in many areas in mathematics, logic and computer science. The Logical Frameworks and Meta-languages: Theory and Practice workshop aims to bring together designers, implementers, and practitioners working on these areas, and in particular about: the automation and implementation of the meta-theory of programming languages and related calculi; the design of proof assistants, automated theorem provers, and formal digital libraries building upon logical framework technology; theoretical and practical issues concerning the encoding of variable binding and fresh name generation, especially the representation of, and reasoning about, datatypes defined from binding signatures; case studies of meta-programming, and the mechanization of the (meta) theory of descriptions of programming languages and other calculi. This volume contains the final and revised versions of the papers presented at LFMTP 2010, which was held on July 14, 2010 in Edinburgh (UK). LFMTP 2010 was part of the Federated Logic Conference (FLoC 2010), and affilated with LICS 2010.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑