Nominal Equational Logic

被引:34
|
作者
Clouston, Ranald A. [1 ]
Pitts, Andrew M. [1 ]
机构
[1] Univ Cambridge, Comp Lab, Cambridge CB3 0DF, England
基金
英国工程与自然科学研究理事会;
关键词
Equational logic; nominal sets; permutation actions; universal algebra;
D O I
10.1016/j.entcs.2007.02.009
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
This paper studies the notion of "freshness" that often occurs in the meta-theory of computer science languages involving various kinds of names. Nominal Equational Logic is an extension of ordinary equational logic with assertions about the freshness of names. It is shown to be both sound and complete for the support interpretation of freshness and equality provided by the Gabbay-Pitts nominal sets model of names, binding and alpha-conversion.
引用
收藏
页码:223 / 257
页数:35
相关论文
共 50 条