A formal treatment of the Barendregt variable convention in rule inductions

Christian Urban; Michael Norrish

doi:10.1145/1088454.1088458

A formal treatment of the Barendregt variable convention in rule inductions

Christian Urban^*, Michael Norrish

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

13 Citations (Scopus)

Abstract

Barendregt's variable convention simplifies many informal proofs in the λ-calculus by allowing the consideration of only those bound variables that have been suitably chosen. Barendregt does not give a formal justification for the variable convention, which makes it hard to formalise such informal proofs. In this paper we show how a form of the variable convention can be built into the reasoning principles for rule inductions. We give two examples explaining our technique.

Original language	English
Title of host publication	MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding
Publisher	Association for Computing Machinery
Pages	25-32
Number of pages	8
ISBN (Print)	1595930728, 9781595930729
DOIs	https://doi.org/10.1145/1088454.1088458
Publication status	Published - 2005
Externally published	Yes
Event	MERLIN'05 - Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding - Tallinn, Estonia Duration: 30 Sept 2005 → 30 Sept 2005

Publication series

Name	MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding

Conference

Conference	MERLIN'05 - Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding
Country/Territory	Estonia
City	Tallinn
Period	30/09/05 → 30/09/05

Access to Document

10.1145/1088454.1088458

Cite this

Urban, C., & Norrish, M. (2005). A formal treatment of the Barendregt variable convention in rule inductions. In MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding (pp. 25-32). (MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding). Association for Computing Machinery. https://doi.org/10.1145/1088454.1088458

Urban, Christian ; Norrish, Michael. / A formal treatment of the Barendregt variable convention in rule inductions. MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding. Association for Computing Machinery, 2005. pp. 25-32 (MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding).

@inproceedings{87bb65093a6f496aabf78213dab06860,

title = "A formal treatment of the Barendregt variable convention in rule inductions",

abstract = "Barendregt's variable convention simplifies many informal proofs in the λ-calculus by allowing the consideration of only those bound variables that have been suitably chosen. Barendregt does not give a formal justification for the variable convention, which makes it hard to formalise such informal proofs. In this paper we show how a form of the variable convention can be built into the reasoning principles for rule inductions. We give two examples explaining our technique.",

keywords = "Lambda-calculus, Nominal logic, POPLmark challenge",

author = "Christian Urban and Michael Norrish",

year = "2005",

doi = "10.1145/1088454.1088458",

language = "English",

isbn = "1595930728",

series = "MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding",

publisher = "Association for Computing Machinery",

pages = "25--32",

booktitle = "MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding",

note = "MERLIN'05 - Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding ; Conference date: 30-09-2005 Through 30-09-2005",

}

Urban, C & Norrish, M 2005, A formal treatment of the Barendregt variable convention in rule inductions. in MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding. MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding, Association for Computing Machinery, pp. 25-32, MERLIN'05 - Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding, Tallinn, Estonia, 30/09/05. https://doi.org/10.1145/1088454.1088458

A formal treatment of the Barendregt variable convention in rule inductions. / Urban, Christian; Norrish, Michael.
MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding. Association for Computing Machinery, 2005. p. 25-32 (MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A formal treatment of the Barendregt variable convention in rule inductions

AU - Urban, Christian

AU - Norrish, Michael

PY - 2005

Y1 - 2005

N2 - Barendregt's variable convention simplifies many informal proofs in the λ-calculus by allowing the consideration of only those bound variables that have been suitably chosen. Barendregt does not give a formal justification for the variable convention, which makes it hard to formalise such informal proofs. In this paper we show how a form of the variable convention can be built into the reasoning principles for rule inductions. We give two examples explaining our technique.

AB - Barendregt's variable convention simplifies many informal proofs in the λ-calculus by allowing the consideration of only those bound variables that have been suitably chosen. Barendregt does not give a formal justification for the variable convention, which makes it hard to formalise such informal proofs. In this paper we show how a form of the variable convention can be built into the reasoning principles for rule inductions. We give two examples explaining our technique.

KW - Lambda-calculus

KW - Nominal logic

KW - POPLmark challenge

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

U2 - 10.1145/1088454.1088458

DO - 10.1145/1088454.1088458

M3 - Conference contribution

SN - 1595930728

SN - 9781595930729

T3 - MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding

SP - 25

EP - 32

BT - MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding

PB - Association for Computing Machinery

T2 - MERLIN'05 - Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding

Y2 - 30 September 2005 through 30 September 2005

ER -

Urban C, Norrish M. A formal treatment of the Barendregt variable convention in rule inductions. In MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding. Association for Computing Machinery. 2005. p. 25-32. (MERLIN'05 - Proceedings of the Third ACM SIGPLAN Workshop in Mechanized Reasoning about Languages with varIable biNding). doi: 10.1145/1088454.1088458

A formal treatment of the Barendregt variable convention in rule inductions

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this