# Publication details

##
Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq

Yannick Forster, Gert Smolka

Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017, April 2017

We formalise a weak call-by-value lambda-calculus we call L in the constructive type theory of Coq and study it as a minimal functional programming language and as a model of computation. We show key results including (1) semantic properties of procedures are undecidable, (2) the class of total procedures is not recognisable, (3) a class is decidable if it is recognisable, corecognisable, and logically decidable, and (4) a class is recognisable if and only if it is enumerable. Most of the results require a step-indexed self-interpreter. All results are verified formally and constructively, which is the challenge of the project. The verification techniques we use for procedures will apply to call-by-value functional programming languages formalised in Coq in general.

*Link to Coq Formalisation*

Download PDF
Show BibTeX

@CONFERENCE{ForsterSmolka:2017:L-Computability,
title = {Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq},
author = {Yannick Forster and Gert Smolka},
year = {2017},
month = {Apr},
booktitle = { Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017},
}

Login to edit

Legal notice, Privacy policy