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
相关论文
共 50 条
  • [31] Nominal logic programming
    Cheney, James
    Urban, Christian
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2008, 30 (05):
  • [32] Parameterized Metareasoning in Membership Equational Logic
    Clavel, Manuel
    Marti-Oliet, Narciso
    Palomino, Miguel
    FORMAL MODELING: ACTORS, OPEN SYSTEMS, BIOLOGICAL SYSTEMS: ESSAYS DEDICATED TO CAROLYN TALCOTT ON THE OCCASION OF HER 70TH BIRTHDAY, 2011, 7000 : 277 - 298
  • [33] Equational Abstractions in Rewriting Logic and Maude
    Marti-Oliet, Narciso
    Duran, Francisco
    Verdejo, Alberto
    FORMAL METHODS: FOUNDATIONS AND APPLICATIONS, SBMF 2014, 2015, 8941 : 17 - 31
  • [34] A spatial equational logic for the applied π-calculus
    Lozes, Etienne
    Villard, Jules
    DISTRIBUTED COMPUTING, 2010, 23 (01) : 61 - 83
  • [35] Specification and proof in membership equational logic
    Bouhoula, A
    Jouannaud, JP
    Meseguer, J
    THEORETICAL COMPUTER SCIENCE, 2000, 236 (1-2) : 35 - 132
  • [36] EQUATIONAL LOGIC AND THEORIES IN SENTENTIAL LANGUAGES
    SUSZKO, R
    COLLOQUIUM MATHEMATICUM, 1974, 29 (01) : 19 - 23
  • [37] Equational logic of recursive program schemes
    Mersch, JG
    ALEBRA AND COALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS, 2005, 3629 : 278 - 292
  • [38] A spatial equational logic for the applied π-calculus
    Étienne Lozes
    Jules Villard
    Distributed Computing, 2010, 23 : 61 - 83
  • [39] A weak form of interpolation in equational logic
    Maksimova, L. L.
    ALGEBRA AND LOGIC, 2008, 47 (01) : 56 - 64
  • [40] ANALYSES OF UNSATISFIABILITY FOR EQUATIONAL LOGIC PROGRAMMING
    ALPUENTE, M
    FALASCHI, M
    MANZO, F
    JOURNAL OF LOGIC PROGRAMMING, 1995, 22 (03): : 223 - 254
12345