Mechanised computability theory

DOI10.1007/978-3-642-22863-6_22MaRDI QIDQ3088013zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Mechanising Turing machines and computability theory in Isabelle/HOL
• Formalization of the computational theory of a Turing complete functional language model
• A Natural Axiomatization of Computability and Proof of Church's Thesis
• Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
• Computability

Cites work

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

Cited in

(20)

• Weak call-by-value lambda calculus as a model of computation in Coq
• Typing total recursive functions in Coq
• Formalization of the computational theory of a Turing complete functional language model
• Parametric Church's thesis: synthetic computability without choice
• Call-by-value lambda calculus as a model of computation in Coq
• Formalizing abstract computability: Turing categories in Coq
• A Coinductive Animation of 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
• scientific article; zbMATH DE number 1236368 (Why is no real title available?)
• scientific article; zbMATH DE number 2102718 (Why is no real title available?)
• Mechanising Turing machines and computability theory in Isabelle/HOL
• An analysis of Tennenbaum's theorem in constructive type theory
• A mechanisation of computability theory in HOL
• Imperative process algebra and models of parallel computation
• Barendregt's theory of the -calculus, refreshed and formalized
• GOL in GOL in HOL: verified circuits in Conway's game of life
• Mechanising Böhm trees and -completeness
• A formalization of multi-tape Turing machines

Describes a project that uses

Uses Software

• Coq
• Isabelle/ZF
• HOL
• HOL Light

This page was built for publication: Mechanised computability theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3088013)