Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings

Jan van Brügge; James McKinna; Andrei Popescu; Dmitriy Traytel

doi:10.1145/3704893

Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings

Jan van Brügge, James McKinna, Andrei Popescu, Dmitriy Traytel

Research output: Contribution to journal › Article › peer-review

1 Citation (Scopus)

4 Downloads (Pure)

Abstract

This paper is a contribution to the meta-theory of systems featuring syntax with bindings, such as -calculi and logics. It provides a general criterion that targets inductively defined rule-based systems, enabling for them inductive proofs that leverage Barendregt's variable convention of keeping the bound and free variables disjoint. It improves on the state of the art by (1) achieving high generality in the style of Knaster-Tarski fixed point definitions (as opposed to imposing syntactic formats), (2) capturing systems of interest without modifications, and (3) accommodating infinitary syntax and non-equivariant predicates.

Original language	English
Article number	57
Journal	Proceedings of the ACM on Programming Languages
Volume	9
Issue number	POPL
DOIs	https://doi.org/10.1145/3704893
Publication status	Published - 9 Jan 2025

Keywords

formal reasoning
induction
nominal sets
syntax with bindings

ASJC Scopus subject areas

Software
Safety, Risk, Reliability and Quality

Access to Document

10.1145/3704893Licence: CC BY

Download pdf
Copyright © 2025 Owner/Author. This work is licensed under a Creative Commons Attribution International 4.0 License.
Final published version, 822 KBLicence: CC BY

Cite this

@article{841932017d5b4e03891e2bfe3d34b631,

title = "Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings",

abstract = "This paper is a contribution to the meta-theory of systems featuring syntax with bindings, such as -calculi and logics. It provides a general criterion that targets inductively defined rule-based systems, enabling for them inductive proofs that leverage Barendregt's variable convention of keeping the bound and free variables disjoint. It improves on the state of the art by (1) achieving high generality in the style of Knaster-Tarski fixed point definitions (as opposed to imposing syntactic formats), (2) capturing systems of interest without modifications, and (3) accommodating infinitary syntax and non-equivariant predicates.",

keywords = "formal reasoning, induction, nominal sets, syntax with bindings",

author = "{van Br{\"u}gge}, Jan and James McKinna and Andrei Popescu and Dmitriy Traytel",

year = "2025",

month = jan,

day = "9",

doi = "10.1145/3704893",

language = "English",

volume = "9",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery",

number = "POPL",

}

TY - JOUR

T1 - Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings

AU - van Brügge, Jan

AU - McKinna, James

AU - Popescu, Andrei

AU - Traytel, Dmitriy

PY - 2025/1/9

Y1 - 2025/1/9

N2 - This paper is a contribution to the meta-theory of systems featuring syntax with bindings, such as -calculi and logics. It provides a general criterion that targets inductively defined rule-based systems, enabling for them inductive proofs that leverage Barendregt's variable convention of keeping the bound and free variables disjoint. It improves on the state of the art by (1) achieving high generality in the style of Knaster-Tarski fixed point definitions (as opposed to imposing syntactic formats), (2) capturing systems of interest without modifications, and (3) accommodating infinitary syntax and non-equivariant predicates.

AB - This paper is a contribution to the meta-theory of systems featuring syntax with bindings, such as -calculi and logics. It provides a general criterion that targets inductively defined rule-based systems, enabling for them inductive proofs that leverage Barendregt's variable convention of keeping the bound and free variables disjoint. It improves on the state of the art by (1) achieving high generality in the style of Knaster-Tarski fixed point definitions (as opposed to imposing syntactic formats), (2) capturing systems of interest without modifications, and (3) accommodating infinitary syntax and non-equivariant predicates.

KW - formal reasoning

KW - induction

KW - nominal sets

KW - syntax with bindings

UR - http://www.scopus.com/inward/record.url?scp=85216220966&partnerID=8YFLogxK

U2 - 10.1145/3704893

DO - 10.1145/3704893

M3 - Article

SN - 2475-1421

VL - 9

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - POPL

M1 - 57

ER -

Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this