DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2025.20

Incremental Computing by Differential Execution

Authors: Prashant Kumar, André Pacak, and Sebastian Erdweg

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract

Incremental computing offers the potential for significant performance gains by efficiently updating computations in response to changing data. However, traditional approaches are either problem-specific or use an inefficient all-or-nothing strategy of rerunning affected computations entirely. This paper presents differential semantics, a novel approach that directly embeds the propagation of changes into the semantics of a general-purpose programming language. Given a precise description of input changes, differential semantics rules define how these changes are tracked and propagated through core language constructs like assignments, conditionals, and loops to produce corresponding output changes. We formalize differential semantics and verify key properties, including correctness, using the Rocq proof assistant. We also develop and formally prove a set of optimizations, particularly for loop handling, that enable asymptotic performance improvements. An implementation of the semantics as a differential interpreter achieves order-of-magnitude speedups over recomputation on the Bellman-Ford shortest path algorithm.

Cite as

Prashant Kumar, André Pacak, and Sebastian Erdweg. Incremental Computing by Differential Execution. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 20:1-20:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kumar_et_al:LIPIcs.ECOOP.2025.20,
  author =	{Kumar, Prashant and Pacak, Andr\'{e} and Erdweg, Sebastian},
  title =	{{Incremental Computing by Differential Execution}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{20:1--20:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.20},
  URN =		{urn:nbn:de:0030-drops-233137},
  doi =		{10.4230/LIPIcs.ECOOP.2025.20},
  annote =	{Keywords: Incremental computing, differential semantics, programming language design, formal verification, big-step semantics}
}

Document

Artifact

DOI: 10.4230/DARTS.11.2.13

Incremental Computing by Differential Execution (Artifact)

Authors: Prashant Kumar, André Pacak, and Sebastian Erdweg

Published in: DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract

This artifact supports the paper titled "Incremental Computing by Differential Execution" accepted at ECOOP 2025. It provides a mechanized formalization in Rocq of the differential semantics and optimizations presented in the paper, along with a reference implementation of the differential interpreter in Scala. The artifact includes the Bellman-Ford benchmark used for the performance evaluation in Section 7. Both components are packaged as Docker images for ease of use and reproducibility, enabling verification of all claims made in the paper.

Cite as

Prashant Kumar, André Pacak, and Sebastian Erdweg. Incremental Computing by Differential Execution (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 13:1-13:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{kumar_et_al:DARTS.11.2.13,
  author =	{Kumar, Prashant and Pacak, Andr\'{e} and Erdweg, Sebastian},
  title =	{{Incremental Computing by Differential Execution (Artifact)}},
  pages =	{13:1--13:8},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2025},
  volume =	{11},
  number =	{2},
  editor =	{Kumar, Prashant and Pacak, Andr\'{e} and Erdweg, Sebastian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.13},
  URN =		{urn:nbn:de:0030-drops-233564},
  doi =		{10.4230/DARTS.11.2.13},
  annote =	{Keywords: Incremental computing, differential semantics, programming language design, formal verification, big-step semantics}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2022.7

Functional Programming with Datalog

Authors: André Pacak and Sebastian Erdweg

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract

Datalog is a carefully restricted logic programming language. What makes Datalog attractive is its declarative fixpoint semantics: Datalog queries consist of simple Horn clauses, yet Datalog solvers efficiently compute all derivable tuples even for recursive queries. However, as we argue in this paper, Datalog is ill-suited as a programming language and Datalog programs are hard to write and maintain. We propose a "new" frontend for Datalog: functional programming with sets called functional IncA. While programmers write recursive functions over algebraic data types and sets, we transparently translate all code to Datalog relations. However, we retain Datalog’s strengths: Functions that generate sets can encode arbitrary relations and mutually recursive functions have fixpoint semantics. We also ensure that the generated Datalog program terminates whenever the original functional program terminates, so that we can apply off-the-shelve bottom-up Datalog solvers. We demonstrate the versatility and ease of use of functional IncA by implementing a type checker, a program transformation, an interpreter of the untyped lambda calculus, two data-flow analyses, and clone detection of Java bytecode.

Cite as

André Pacak and Sebastian Erdweg. Functional Programming with Datalog. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 7:1-7:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{pacak_et_al:LIPIcs.ECOOP.2022.7,
  author =	{Pacak, Andr\'{e} and Erdweg, Sebastian},
  title =	{{Functional Programming with Datalog}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{7:1--7:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.7},
  URN =		{urn:nbn:de:0030-drops-162354},
  doi =		{10.4230/LIPIcs.ECOOP.2022.7},
  annote =	{Keywords: Datalog, functional programming, demand transformation}
}

Search Results

Documents authored by Pacak, André

Incremental Computing by Differential Execution

Abstract

Cite as

Incremental Computing by Differential Execution (Artifact)

Abstract

Cite as

Functional Programming with Datalog

Abstract

Cite as

Thanks for your feedback!

Could not send message