From Undecidability.L Require Import L.

(* Problems concerning the call-by-value lambda-calculus *)

(* Call-by-Value Lambda Calculus as a Model of Computation in Coq. Yannick Forster and Gert Smolka. Journal of Automated Reasoning (2018). https://www.ps.uni-saarland.de/extras/L-computability/ *)

About eva. (* Halting problem for call-by-value lambda-calculus *)
