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

DOI10.1007/978-3-319-66107-0_13MaRDI QIDQ1687735zbMATH OpenOpenAlexFDO

Authors Yannick Forster, Gert Smolka

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

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

Recommendations

• Call-by-value lambda calculus as a model of computation in Coq
• Formal small-step verification of a call-by-value lambda calculus machine
• Open call-by-value
• The weak lambda calculus as a reasonable machine
• Formal verification of the correspondence between call-by-need and call-by-name

Cites work

• scientific article; zbMATH DE number 1033559 (Why is no real title available?)
• scientific article; zbMATH DE number 1517989 (Why is no real title available?)
• A Declarative Language for the Coq Proof Assistant
• A formalization of multi-tape Turing machines
• Computability and Logic
• Efficient self-interpretation in lambda calculus
• First steps in synthetic computability theory
• Formalizing Turing Machines
• Mechanised computability theory
• Mechanising Turing machines and computability theory in Isabelle/HOL
• Programming in the λ-Calculus: From Church to Scott and Back
• The independence of Markov's principle in type theory
• The weak lambda calculus as a reasonable machine

Cited in

(9)

• Call-by-value lambda calculus as a model of computation in Coq
• scientific article; zbMATH DE number 7566048 (Why is no real title available?)
• The \textsc{MetaCoq} project
• Formalizing abstract computability: Turing categories in Coq
• The weak lambda calculus as a reasonable machine
• Open call-by-value
• Parametric Church's thesis: synthetic computability without choice
• Hilbert's Tenth Problem in Coq
• Formalization of the computational theory of a Turing complete functional language model

Describes a project that uses

Uses Software

• Coq

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

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