2018/10/19 by Yannick Forster, Gert Smolka · 1 citation
Computer Science · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge #Computability, Logic, AI Algorithms
paper · doi:10.1007/s10817-018-9484-2
openalex publication_date 2018/10/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We formalise a (weak) call-by-value λ -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.