Mechanising λ-calculus using a classical first order theory of terms with permutations

Michael Norrish

doi:10.1007/s10990-006-8745-7

Mechanising λ-calculus using a classical first order theory of terms with permutations

Michael Norrish^*

^*Corresponding author for this work

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

18 Citations (Scopus)

Abstract

This paper describes the mechanisation in HOL of some basic λ-calculus theory. The proofs are taken from standard sources (books by Hankin and Barendregt), and cover: equational theory, reduction theory, residuals, finiteness of developments, and the standardisation theorem. The issues in mechanising pen-and-paper proofs are discussed; in particular, those difficulties arising from the sources' use of the Barendregt Variable Convention.

Original language	English
Pages (from-to)	169-195
Number of pages	27
Journal	Higher-Order and Symbolic Computation
Volume	19
Issue number	2-3
DOIs	https://doi.org/10.1007/s10990-006-8745-7
Publication status	Published - Sept 2006

Access to Document

10.1007/s10990-006-8745-7

Cite this

@article{80138a2ffa1b4e2ca05a7f5693ab10d0,

title = "Mechanising λ-calculus using a classical first order theory of terms with permutations",

abstract = "This paper describes the mechanisation in HOL of some basic λ-calculus theory. The proofs are taken from standard sources (books by Hankin and Barendregt), and cover: equational theory, reduction theory, residuals, finiteness of developments, and the standardisation theorem. The issues in mechanising pen-and-paper proofs are discussed; in particular, those difficulties arising from the sources' use of the Barendregt Variable Convention.",

author = "Michael Norrish",

year = "2006",

month = sep,

doi = "10.1007/s10990-006-8745-7",

language = "English",

volume = "19",

pages = "169--195",

journal = "Higher-Order and Symbolic Computation",

issn = "1388-3690",

publisher = "Springer Netherlands",

number = "2-3",

}

TY - JOUR

T1 - Mechanising λ-calculus using a classical first order theory of terms with permutations

AU - Norrish, Michael

PY - 2006/9

Y1 - 2006/9

N2 - This paper describes the mechanisation in HOL of some basic λ-calculus theory. The proofs are taken from standard sources (books by Hankin and Barendregt), and cover: equational theory, reduction theory, residuals, finiteness of developments, and the standardisation theorem. The issues in mechanising pen-and-paper proofs are discussed; in particular, those difficulties arising from the sources' use of the Barendregt Variable Convention.

AB - This paper describes the mechanisation in HOL of some basic λ-calculus theory. The proofs are taken from standard sources (books by Hankin and Barendregt), and cover: equational theory, reduction theory, residuals, finiteness of developments, and the standardisation theorem. The issues in mechanising pen-and-paper proofs are discussed; in particular, those difficulties arising from the sources' use of the Barendregt Variable Convention.

UR - https://www.scopus.com/pages/publications/33747268056

U2 - 10.1007/s10990-006-8745-7

DO - 10.1007/s10990-006-8745-7

M3 - Article

SN - 1388-3690

VL - 19

SP - 169

EP - 195

JO - Higher-Order and Symbolic Computation

JF - Higher-Order and Symbolic Computation

IS - 2-3

ER -

Mechanising λ-calculus using a classical first order theory of terms with permutations

Abstract

Access to Document

Other files and links

Fingerprint

Cite this