You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: University of Leicester » Outputs » Detail

Output details

11 - Computer Science and Informatics

University of Leicester

Return to search Previous output Next output

Output 6 of 71 in the submission

Article title

Alpha equivalence equalities

Type

D - Journal article

DOI

10.1016/j.tcs.2012.01.030

Title of journal

Theoretical Computer Science

Article number

Volume number

433

Issue number

First page of article

ISSN of journal

0304-3975

Year of publication

2012

URL

Number of additional authors

Additional information

<10> We give abstract formalisations of alpha-equivalence. Concrete instances have played a crucial role in machine verification applications, and related areas. Gabbay (Nominal Semantics for Predicate Logic, 2012) observes some useful instances of our general results. Significantly, we note proof errors in the current literature, and correct them using an especially rigorous approach that may serve as a future basis for implementation in a theorem prover. Urban (Nominal Unification, 2004) addresses a practical application of "nominal program contexts": we develop a novel "permutation context" that subsumes and extends this 2004 definition.

Interdisciplinary

Cross-referral requested

Research group

None

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract