逻辑专栏14：名义逻辑与抽象语法
摘要：正式化逻辑、编程语言、安全协议和其他形式化系统的句法证明是一个重大挑战，主要是因为需要正确处理名称绑定的义务。我们提出了一种称为名义抽象语法的方法，自其大约六年前引入以来，已经引起了相当大的兴趣。在概述其他方法之后，我们描述了名义抽象语法和名义逻辑，名义逻辑用于推理名义抽象语法。我们还讨论了名义技术在编程、自动推理中的应用，并确定了一些未来的方向。
作者：James Cheney
论文ID：cs/0511025
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23