Weak call-by-value lambda calculus as a model of computation in Coq
type: Item
instance of: scholarly article
title: Weak call-by-value lambda calculus as a model of computation in Coq
zbMATH Open document ID: 1468.68322
DOI: 10.1007/978-3-319-66107-0_13
author: Yannick Forster
author: Gert Smolka
publication date: 2018-01-04T00:00:00Z
Mathematics Subject Classification ID: 68V20
Mathematics Subject Classification ID: 68N18
Mathematics Subject Classification ID: 68Q04
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 6821852
describes a project that uses: Coq
MaRDI profile type: Publication
full work available at URL: 978-3-319-66107-0 13
OpenAlex ID: W2895928777
cites work: Formalizing Turing Machines
cites work: A formalization of multi-tape Turing machines
cites work: First steps in synthetic computability theory
cites work: Computability and Logic
cites work: The Independence of Markov's Principle in Type Theory.
cites work: The weak lambda calculus as a reasonable machine
cites work: Q4506483
cites work: Programming in the λ-Calculus: From Church to Scott and Back
cites work: Q4344149
cites work: Efficient self-interpretation in lambda calculus
cites work: Mechanised Computability Theory
cites work: A Declarative Language for the Coq Proof Assistant
cites work: Mechanising Turing Machines and Computability Theory in Isabelle/HOL
description: scientific article; zbMATH DE number 6821852