2026-07-21T23:17:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24606 2025-12-12T15:09:52Z ddc:004 open_access

A Verified Cost Model for Call-By-Push-Value Chen, Zhuo Zoey Åman Pohjola, Johannes Rizkallah, Christine lambda calculus formalizations of computational models computability theory HOL call-by-push-value reduction time and space complexity abstract machines The call-by-push-value λ-calculus allows for syntactically specifying the order of evaluation as part of the term language. Hence, it serves as a unifying language for embedding various evaluation strategies including call-by-value and call-by-name. Given the impact of call-by-push-value, it is remarkable that its adequacy as a model for computational complexity theory has not yet been studied. In this paper, we show that the call-by-push-value λ-calculus is reasonable for both time and space complexity. A reasonable cost model can encode other reasonable cost models with polynomial overhead in time and constant factor overhead in space. We achieve this by encoding call-by-push-value λ-calculus into Turing machines, following a simulation strategy by Forster et al.; for the converse direction, we prove that Levy’s encoding of the call-by-value λ-calculus has reasonable complexity bounds. The main results have been formalised in the HOL4 theorem prover. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Zhuo Zoey Chen and Johannes Åman Pohjola and Christine Rizkallah 2025 Is Part Of LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2025.7 urn:nbn:de:0030-drops-246067 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.7 eng https://creativecommons.org/licenses/by/4.0/legalcode