Mechanising lambda-calculus using a classical first order theory of terms with permutations
-
Altmetric Citations
Description
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 sta
Collections | ANU Research Publications |
---|---|
Date published: | 2006 |
Type: | Journal article |
URI: | http://hdl.handle.net/1885/31081 |
Source: | Higher-Order and Symbolic Computation |
DOI: | 10.1007/s10990-006-8745-7 |
Download
File | Description | Size | Format | Image |
---|---|---|---|---|
01_Norrish_Mechanising_lambda-calculus_2006.pdf | 293.3 kB | Adobe PDF | Request a copy |
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.
Updated: 17 November 2022/ Responsible Officer: University Librarian/ Page Contact: Library Systems & Web Coordinator