7 Search Results for "Åman Pohjola, Johannes"

Artifact
Software
DOI: 10.4230/artifacts.24718
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}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.15
A Verified Cyclicity Checker: For Theories with Overloaded Constants

Authors: Arve Gengelbach and Johannes Åman Pohjola

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
Non-terminating (dependencies of) definitions can lead to logical contradictions, for example when defining a boolean constant as its own negation. Some proof assistants thus detect and disallow non-terminating definitions. Termination is generally undecidable when constants may have different definitions at different type instances, which is called (ad-hoc) overloading. The Isabelle/HOL proof assistant supports overloading of constant definitions, but relies on an unclear foundation for this critical termination check. With this paper we aim to close this gap: we present a mechanised proof that, for restricted overloading, non-terminating definitions are of a detectable cyclic shape, and we describe a mechanised algorithm with its correctness proof. In addition we demonstrate this cyclicity checker on parts of the Isabelle/HOL main library. Furthermore, we introduce the first-ever formally verified kernel of a proof assistant for higher-order logic with overloaded definitions. All our results are formalised in the HOL4 theorem prover.
Cite as

Arve Gengelbach and Johannes Åman Pohjola. A Verified Cyclicity Checker: For Theories with Overloaded Constants. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gengelbach_et_al:LIPIcs.ITP.2022.15,
  author =	{Gengelbach, Arve and \r{A}man Pohjola, Johannes},
  title =	{{A Verified Cyclicity Checker: For Theories with Overloaded Constants}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.15},
  URN =		{urn:nbn:de:0030-drops-167240},
  doi =		{10.4230/LIPIcs.ITP.2022.15},
  annote =	{Keywords: cyclicity, non-termination, ad-hoc overloading, definitions, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.27
Kalas: A Verified, End-To-End Compiler for a Choreographic Language

Authors: Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, and Michael Norrish

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
Choreographies are an abstraction for globally describing deadlock-free communicating systems. A choreography can be compiled into multiple endpoints preserving the global behavior, providing a path for concrete system implementations. Of course, the soundness of this approach hinges on the correctness of the compilation function. In this paper, we present a verified compiler for Kalas, a choreographic language. Its machine-checked end-to-end proof of correctness ensures all generated endpoints adhere to the system description, preserving the top-level communication guarantees. This work uses the verified CakeML compiler and Hol4 proof assistant, allowing for concrete executable implementations and statements of correctness at the machine code level for multiple architectures.
Cite as

Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, and Michael Norrish. Kalas: A Verified, End-To-End Compiler for a Choreographic Language. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{pohjola_et_al:LIPIcs.ITP.2022.27,
  author =	{Pohjola, Johannes \r{A}man and G\'{o}mez-Londo\~{n}o, Alejandro and Shaker, James and Norrish, Michael},
  title =	{{Kalas: A Verified, End-To-End Compiler for a Choreographic Language}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{27:1--27:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.27},
  URN =		{urn:nbn:de:0030-drops-167368},
  doi =		{10.4230/LIPIcs.ITP.2022.27},
  annote =	{Keywords: Choreographies, Interactive Theorem Proving, Compiler Verification}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.ITP.2021.1
The CakeML Project’s Quest for Ever Stronger Correctness Theorems (Invited Paper)

Authors: Magnus O. Myreen

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
The CakeML project has developed a proof-producing code generation mechanism for the HOL4 theorem prover, a verified compiler for ML and, using these, a number of verified application programs that are proved correct down to the machine code that runs them (in some cases, even down to the underlying hardware). The purpose of this extended abstract is to tell the story of the project and to point curious readers to publications where they can read more about specific contributions.
Cite as

Magnus O. Myreen. The CakeML Project’s Quest for Ever Stronger Correctness Theorems (Invited Paper). In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 1:1-1:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{myreen:LIPIcs.ITP.2021.1,
  author =	{Myreen, Magnus O.},
  title =	{{The CakeML Project’s Quest for Ever Stronger Correctness Theorems}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{1:1--1:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.1},
  URN =		{urn:nbn:de:0030-drops-138963},
  doi =		{10.4230/LIPIcs.ITP.2021.1},
  annote =	{Keywords: Program verification, interactive theorem proving}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.27
Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security

Authors: Robert Sison and Toby Murray

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
It is common to prove by reasoning over source code that programs do not leak sensitive data. But doing so leaves a gap between reasoning and reality that can only be filled by accounting for the behaviour of the compiler. This task is complicated when programs enforce value-dependent information-flow security properties (in which classification of locations can vary depending on values in other locations) and complicated further when programs exploit shared-variable concurrency. Prior work has formally defined a notion of concurrency-aware refinement for preserving value-dependent security properties. However, that notion is considerably more complex than standard refinement definitions typically applied in the verification of semantics preservation by compilers. To date it remains unclear whether it can be applied to a realistic compiler, because there exist no general decomposition principles for separating it into smaller, more familiar, proof obligations. In this work, we provide such a decomposition principle, which we show can almost halve the complexity of proving secure refinement. Further, we demonstrate its applicability to secure compilation, by proving in Isabelle/HOL the preservation of value-dependent security by a proof-of-concept compiler from an imperative While language to a generic RISC-style assembly language, for programs with shared-memory concurrency mediated by locking primitives. Finally, we execute our compiler in Isabelle on a While language model of the Cross Domain Desktop Compositor, demonstrating to our knowledge the first use of a compiler verification result to carry an information-flow security property down to the assembly-level model of a non-trivial concurrent program.
Cite as

Robert Sison and Toby Murray. Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{sison_et_al:LIPIcs.ITP.2019.27,
  author =	{Sison, Robert and Murray, Toby},
  title =	{{Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{27:1--27:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.27},
  URN =		{urn:nbn:de:0030-drops-110829},
  doi =		{10.4230/LIPIcs.ITP.2019.27},
  annote =	{Keywords: Secure compilation, Information flow security, Concurrency, Verification}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.32
Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs

Authors: Johannes Åman Pohjola, Henrik Rostedt, and Magnus O. Myreen

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
There are useful programs that do not terminate, and yet standard Hoare logics are not able to prove liveness properties about non-terminating programs. This paper shows how a Hoare-like programming logic framework (characteristic formulae) can be extended to enable reasoning about the I/O behaviour of programs that do not terminate. The approach is inspired by transfinite induction rather than coinduction, and does not require non-terminating loops to be productive. This work has been developed in the HOL4 theorem prover and has been integrated into the ecosystem of proof tools surrounding the CakeML programming language.
Cite as

Johannes Åman Pohjola, Henrik Rostedt, and Magnus O. Myreen. Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{amanpohjola_et_al:LIPIcs.ITP.2019.32,
  author =	{\r{A}man Pohjola, Johannes and Rostedt, Henrik and Myreen, Magnus O.},
  title =	{{Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{32:1--32:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.32},
  URN =		{urn:nbn:de:0030-drops-110872},
  doi =		{10.4230/LIPIcs.ITP.2019.32},
  annote =	{Keywords: Program verification, non-termination, liveness, Hoare logic}
}
  • Refine by Type
  • 6 Document/PDF
  • 1 Artifact
  • 1 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 2 2022
  • 1 2021
  • 2 2019

  • Refine by Author
  • 4 Åman Pohjola, Johannes
  • 2 Chen, Zhuo Zoey
  • 2 Myreen, Magnus O.
  • 2 Rizkallah, Christine
  • 1 Gengelbach, Arve
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs

  • Refine by Classification
  • 3 Theory of computation → Higher order logic
  • 2 Software and its engineering → Compilers
  • 2 Software and its engineering → Software verification
  • 1 Security and privacy → Information flow control
  • 1 Security and privacy → Logic and verification
  • Show More...

  • Refine by Keyword
  • 2 Program verification
  • 2 non-termination
  • 1 Choreographies
  • 1 Compiler Verification
  • 1 Concurrency
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact