Nominal Equational Logic

被引：34
作者：
Clouston, Ranald A. [1 ]
Pitts, Andrew M. [1 ]
机构：
[1] Univ Cambridge, Comp Lab, Cambridge CB3 0DF, England
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2007年 / 172卷
基金：
英国工程与自然科学研究理事会;
关键词：
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
相关论文
共 33 条
  • [1] Nominal games and full abstraction for the nu-calculus
    Abramsky, S
    Ghica, DR
    Murawski, AS
    Ong, CHL
    Stark, IDB
    [J]. 19TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2004, : 150 - 159
  • [2] Barendregt H. P, 1984, LAMBDA CALCULUS ITS
  • [3] BERGER U, 1991, SIXTH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, P203
  • [4] Completeness and Herbrand theorems for nominal logic
    Cheney, J
    [J]. JOURNAL OF SYMBOLIC LOGIC, 2006, 71 (01) : 299 - 320
  • [5] αProlog:: A logic programming language with names, binding and α-equivalence
    Cheney, J
    Urban, C
    [J]. LOGIC PROGRAMMING, PROCEEDINGS, 2004, 3132 : 269 - 283
  • [6] Cheney J, 2004, THESIS
  • [7] Dybjer P, 2002, LECT NOTES COMPUT SC, V2395, P137
  • [8] Fernandez M., 2004, PROC PPDP, P108
  • [9] A congruence rule format for name-passing process calculi from mathematical structural operational semantics
    Fiore, Marcelo
    Staton, Sam
    [J]. 21ST ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2006, : 49 - +
  • [10] FIORE MP, 1999, 14 ANN S LOG COMP SC, P193, DOI DOI 10.1109/LICS.1999.782615
1234