DROPS

Artifact

Software

cbpv-reasonable-HOL

Authors: Zhuo Zoey Chen, Johannes Åman Pohjola, and Christine Rizkallah

Abstract

Cite as

Zhuo Zoey Chen, Johannes Åman Pohjola, Christine Rizkallah. cbpv-reasonable-HOL (Software, Mechanised Proof). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24718,
   title = {{cbpv-reasonable-HOL}}, 
   author = {Chen, Zhuo Zoey and \r{A}man Pohjola, Johannes and Rizkallah, Christine},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:df18377e9fa5e35255f2687ad66ddbc2f010b934;origin=https://github.com/ZhuoZoeyChen/cbpv-reasonable-HOL;visit=swh:1:snp:9fefd6f03db3694a8bdc7e5ea8ff0f4a1fbde680;anchor=swh:1:rev:4e4f4692c9e6e1e23c566ec4730f81eafde32f3c}{\texttt{swh:1:dir:df18377e9fa5e35255f2687ad66ddbc2f010b934}} (visited on 2025-09-22)},
   url = {https://github.com/ZhuoZoeyChen/cbpv-reasonable-HOL/},
   doi = {10.4230/artifacts.24718},
}

Document

DOI: 10.4230/LIPIcs.ITP.2025.7

A Verified Cost Model for Call-By-Push-Value

Authors: Zhuo Zoey Chen, Johannes Åman Pohjola, and Christine Rizkallah

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract

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.

Cite as

Zhuo Zoey Chen, Johannes Åman Pohjola, and Christine Rizkallah. A Verified Cost Model for Call-By-Push-Value. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.ITP.2025.7,
  author =	{Chen, Zhuo Zoey and \r{A}man Pohjola, Johannes and Rizkallah, Christine},
  title =	{{A Verified Cost Model for Call-By-Push-Value}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.7},
  URN =		{urn:nbn:de:0030-drops-246067},
  doi =		{10.4230/LIPIcs.ITP.2025.7},
  annote =	{Keywords: lambda calculus, formalizations of computational models, computability theory, HOL, call-by-push-value reduction, time and space complexity, abstract machines}
}

Search Results

Documents authored by Chen, Zhuo Zoey

cbpv-reasonable-HOL

Abstract

Cite as

A Verified Cost Model for Call-By-Push-Value

Abstract

Cite as

Thanks for your feedback!

Could not send message