Skip navigation
Skip navigation

On the role of names in reasoning about lambda-tree syntax specifications

Tiu, Alwen

Description

Lambda tree syntax (a variant of HOAS) and nominal techniques are two approaches to representing and reasoning about languages containing bindings. Although they are based on separate foundations, recent advances in the proof theory of generic judgments have shown that one may be able to incorporate some aspects of nominal techniques (i.e., the equivariant principle) to simplify reasoning about λ-tree syntax specifications, while still maintaining the crucial aspects of λ-tree syntax. In this...[Show more]

dc.contributor.authorTiu, Alwen
dc.date.accessioned2015-12-10T22:50:32Z
dc.identifier.issn1571-0661
dc.identifier.urihttp://hdl.handle.net/1885/58666
dc.description.abstractLambda tree syntax (a variant of HOAS) and nominal techniques are two approaches to representing and reasoning about languages containing bindings. Although they are based on separate foundations, recent advances in the proof theory of generic judgments have shown that one may be able to incorporate some aspects of nominal techniques (i.e., the equivariant principle) to simplify reasoning about λ-tree syntax specifications, while still maintaining the crucial aspects of λ-tree syntax. In this paper, we present a logic, called LGnω, which incorporates a notion of generic judgments and equivariant reasoning. The logic LGnω is a simple extension of a logic called LGω by Tiu, and can be seen as a special case of the logic G by Gacek, Miller and Nadathur. A central idea of LGnω is the representation of a data type for names (represented by a predicate). Although the data type is inhabited by infinitely many elements, the judgments of the logic only ever use finitely many of them, and more importantly, validity of these judgments are preserved under arbitrary permutation of names, i.e., they are equivariant judgments. This finite support of judgments allows for tractable introduction rules of the name predicate. We illustrate with two examples how this simple extension can be used for reasoning about specifications involving bindings. In the first example, we show how one can represent the data type for λ-terms, and derive a structural induction principle for inductive reasoning over λ-terms. In the second example, we re-examine previous known encodings of open and late bisimulations for the π-calculus. We show that the difference between open and late bisimulation can be characterized by the choice of the encodings of names: the "untyped" version (for the former) versus the "typed" one (for the latter).
dc.publisherElsevier
dc.sourceElectronic Notes in Theoretical Computer Science
dc.subjectKeywords: Encoding (symbols); Fault tolerance; Functions; Quality assurance; Reliability; Specifications; Syntactics; bisimulation; generic judgments; logical framework; nominal techniques; pi-calculus; Calculations bisimulation; generic judgments; logical framework; nominal techniques; pi-calculus
dc.titleOn the role of names in reasoning about lambda-tree syntax specifications
dc.typeJournal article
local.description.notesImported from ARIES
local.identifier.citationvolume228
dc.date.issued2009
local.identifier.absfor080203 - Computational Logic and Formal Languages
local.identifier.ariespublicationu8803936xPUB452
local.type.statusPublished Version
local.contributor.affiliationTiu, Alwen, College of Engineering and Computer Science, ANU
local.description.embargo2037-12-31
local.bibliographicCitation.startpage135
local.bibliographicCitation.lastpage150
local.identifier.doi10.1016/j.entcs.2008.12.122
dc.date.updated2016-02-24T11:45:07Z
local.identifier.scopusID2-s2.0-58149373530
CollectionsANU Research Publications

Download

File Description SizeFormat Image
01_Tiu_On_the_role_of_names_in_2009.pdf248.72 kBAdobe PDF    Request a copy
02_Tiu_On_the_role_of_names_in_2009.pdf163.63 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator