Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Asperti, A., Ricciotti, W.: Formalizing turing machines. In: Ong, L., Queiroz, R. (eds.) WoLLIC 2012. LNCS, vol. 7456, pp. 1–25. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32621-9_1
Asperti, A., Ricciotti, W.: A formalization of multi-tape turing machines. Theoret. Comput. Sci. 603, 23–42 (2015)
Barendregt, H.P., Calculus, T.L.: Its Syntax and Semantics, 2 revised edn. North-Holland, Amsterdam (1984)
Bauer, A.: First steps in synthetic computability theory. ENTCS 155, 5–31 (2006)
Boolos, G., Burgess, J.P., Jeffrey, R.C.: Computability and Logic, 5th edn. Cambridge University Press, Cambridge (2007)
Ciaffaglione, A.: Towards turing computability via coinduction. Sci. Comput. Program. 126, 31–51 (2016)
Coquand, T., Mannaa, B.: The independence of Markov’s principle in type theory. In: FSCD 2016. LIPIcs, vol. 52, pp. 17:1–17:18. Schloss Dagstuhl (2016)
Dal Lago, U., Martini, S.: The weak lambda calculus as a reasonable machine. Theor. Comput. Sci. 398(1–3), 32–50 (2008)
Hopcroft, J., Motwani, R., Ullman, J.: Introduction to Automata Theory, Languages, and Computation. Pearson, New York (2013)
Jansen, J.M.: Programming in the \(\lambda \)-calculus: from church to scott and back. In: Achten, P., Koopman, P. (eds.) The Beauty of Functional Code. LNCS, vol. 8106, pp. 168–180. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40355-2_12
Kozen, D.: Automata and Computability. Springer, New York (1997)
Mogensen, T.Æ.: Efficient self-interpretations in lambda calculus. J. Funct. Program. 2(3), 345–363 (1992)
Niehren, J.: Functional computation as concurrent computation. In: POPL 1996, pp. 333–343. ACM (1996)
Norrish, M.: Mechanised computability theory. In: Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 297–311. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22863-6_22
The Coq Proof Assistant. http://coq.inria.fr
Xu, J., Zhang, X., Urban, C.: Mechanising turing machines and computability theory in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 147–162. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39634-2_13
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Forster, Y., Smolka, G. (2017). Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017. Lecture Notes in Computer Science(), vol 10499. Springer, Cham. https://doi.org/10.1007/978-3-319-66107-0_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-66107-0_13
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66106-3
Online ISBN: 978-3-319-66107-0
eBook Packages: Computer ScienceComputer Science (R0)