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 *)
(* 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 *)