Weak call-by-value lambda calculus as a model of computation in Coq

DOI10.1007/978-3-319-66107-0_13zbMath1468.68322OpenAlexW2895928777MaRDI QIDQ1687735

Gert Smolka, Yannick Forster

Publication date: 4 January 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-66107-0_13

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20) Classical models of computation (Turing machines, etc.) (68Q04)

Related Items (7)

Parametric Church's thesis: synthetic computability without choice ⋮ The \textsc{MetaCoq} project ⋮ Unnamed Item ⋮ Hilbert's Tenth Problem in Coq ⋮ Call-by-value lambda calculus as a model of computation in Coq ⋮ Formalizing abstract computability: Turing categories in Coq ⋮ Formalization of the computational theory of a Turing complete functional language model

Uses Software

• Coq

Cites Work

• A formalization of multi-tape Turing machines
• The weak lambda calculus as a reasonable machine
• Formalizing Turing Machines
• Mechanised Computability Theory
• A Declarative Language for the Coq Proof Assistant
• Computability and Logic
• Efficient self-interpretation in lambda calculus
• Mechanising Turing Machines and Computability Theory in Isabelle/HOL
• The Independence of Markov's Principle in Type Theory.
• Programming in the λ-Calculus: From Church to Scott and Back
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Weak call-by-value lambda calculus as a model of computation in Coq