Mechanised Computability Theory

DOI10.1007/978-3-642-22863-6_22zbMath1342.68299OpenAlexW2133921140MaRDI QIDQ3088013

Michael Norrish

Publication date: 17 August 2011

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22863-6_22

Mathematics Subject Classification ID

Recursive functions and relations, subrecursive hierarchies (03D20) Recursively (computably) enumerable sets and degrees (03D25) Combinatory logic and lambda calculus (03B40)

Related Items (10)

Parametric Church's thesis: synthetic computability without choice ⋮ Weak call-by-value lambda calculus as a model of computation in Coq ⋮ Typing total recursive functions in Coq ⋮ A Coinductive Animation of Turing Machines ⋮ A formalization of multi-tape Turing machines ⋮ Incompleteness, Undecidability and Automated Proofs ⋮ Constructive Formalization of Hybrid Logic with Eventualities ⋮ Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem ⋮ Call-by-value lambda calculus as a model of computation in Coq ⋮ Formalization of the computational theory of a Turing complete functional language model

Uses Software

• Coq
• Isabelle/ZF
• HOL
• HOL Light

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
• Mechanizing the metatheory of LF
• HOL Light: An Overview
• Proof Pearl: De Bruijn Terms Really Do Work
• Metamathematics, Machines and Gödel's Proof
• Theorem Proving in Higher Order Logics

This page was built for publication: Mechanised Computability Theory