5 Search Results for "Costa Seco, João"

Document
DOI: 10.4230/LIPIcs.ECOOP.2025.10
Bottom-Up Synthesis of Memory Mutations with Separation Logic

Authors: Kasra Ferdowsi and Hila Peleg

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

Abstract
Programming-by-Example (PBE) is the paradigm of program synthesis specified via input-output pairs. It is commonly used because examples are easy to provide and collect from the environment. A popular optimization for enumerative synthesis with examples is Observational Equivalence (OE), which groups programs into equivalence classes according to their evaluation on example inputs. Current formulations of OE, however, are severely limited by the assumption that the synthesizer’s target language contains only pure components with no side-effects, either enforcing this in their target language, or ignoring it, leading to an incorrect enumeration. This limits their ability to use realistic component sets. We address this limitation by borrowing from Separation Logic, which can compositionally reason about heap mutations. We reformulate PBE using a restricted Separation Logic: Concrete Heap Separation Logic (CHSL), transforming the search for programs into a proof search in CHSL. This lets us perform bottom-up enumerative synthesis without the need for expert-provided annotations or domain-specific inferences, but with three key advantages: we (i) preserve correctness in the presence of memory-mutating operations, (ii) compact the search space by representing many concrete programs as one under CHSL, and (iii) perform a provably correct OE-reduction. We present SObEq (Side-effects in OBservational EQuivalence), a bottom-up enumerative algorithm that, given a PBE task, searches for its CHSL derivation. The SObEq algorithm is proved correct with no purity assumptions: we show it is guaranteed to lose no solutions. We also evaluate our implementation of SObEq on benchmarks from the literature and online sources, and show that it produces high-quality results quickly.
Cite as

Kasra Ferdowsi and Hila Peleg. Bottom-Up Synthesis of Memory Mutations with Separation Logic. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 10:1-10:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ferdowsi_et_al:LIPIcs.ECOOP.2025.10,
  author =	{Ferdowsi, Kasra and Peleg, Hila},
  title =	{{Bottom-Up Synthesis of Memory Mutations with Separation Logic}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{10:1--10:32},
  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.10},
  URN =		{urn:nbn:de:0030-drops-233036},
  doi =		{10.4230/LIPIcs.ECOOP.2025.10},
  annote =	{Keywords: Program synthesis, observational equivalence}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.9
A Language-Based Version Control System for Python

Authors: Luís Carvalho and João Costa Seco

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
We extend prior work on a language-based approach to versioned software development to support versioned programs with mutable state and evolving method interfaces. Unlike the traditional approach of mainstream version control systems, where a textual diff represents each evolution step, we treat versions as programming elements. Each evolution step, merge operation, and version relationship is represented explicitly in a multifaceted code representation. This provides static guarantees for safe code reuse from previous versions and forward and backwards compatibility between versions, allowing clients to use newly introduced code without needing to refactor their program manually. By lifting versioning to the language level, we pave the way for tools that interact with software repositories to have more insight into a system’s behavior evolution. We instantiate our work in the Python programming language and demonstrate its applicability regarding common evolution and refactoring patterns found in different versions of popular Python packages.
Cite as

Luís Carvalho and João Costa Seco. A Language-Based Version Control System for Python. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 9:1-9:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{carvalho_et_al:LIPIcs.ECOOP.2024.9,
  author =	{Carvalho, Lu{\'\i}s and Costa Seco, Jo\~{a}o},
  title =	{{A Language-Based Version Control System for Python}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{9:1--9:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.9},
  URN =		{urn:nbn:de:0030-drops-208586},
  doi =		{10.4230/LIPIcs.ECOOP.2024.9},
  annote =	{Keywords: Software evolution, type theory}
}
Document
Artifact
DOI: 10.4230/DARTS.10.2.3
A Language-Based Version Control System for Python (Artifact)

Authors: Luís Carvalho and João Costa Seco

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
We extend prior work on a language-based approach to versioned software development to support versioned programs with mutable state and evolving method interfaces. Unlike the traditional approach of mainstream version control systems, where a textual diff represents each evolution step, we treat versions as programming elements. Each evolution step, merge operation, and version relationship is represented explicitly in a multifaceted code representation. This provides static guarantees for safe code reuse from previous versions and forward and backwards compatibility between versions, allowing clients to use newly introduced code without needing to refactor their program manually. By lifting versioning to the language level, we pave the way for tools that interact with software repositories to have more insight into a system’s behavior evolution. We instantiate our work in the Python programming language and demonstrate its applicability regarding common evolution and refactoring patterns found in different versions of popular Python packages.
Cite as

Luís Carvalho and João Costa Seco. A Language-Based Version Control System for Python (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{carvalho_et_al:DARTS.10.2.3,
  author =	{Carvalho, Lu{\'\i}s and Costa Seco, Jo\~{a}o},
  title =	{{A Language-Based Version Control System for Python (Artifact)}},
  pages =	{3:1--3:2},
  journal =	{Dagstuhl Artifacts Series},
  ISBN =	{978-3-95977-342-3},
  ISSN =	{2509-8195},
  year =	{2024},
  volume =	{10},
  number =	{2},
  editor =	{Carvalho, Lu{\'\i}s and Costa Seco, Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.3},
  URN =		{urn:nbn:de:0030-drops-209017},
  doi =		{10.4230/DARTS.10.2.3},
  annote =	{Keywords: Software evolution, type theory}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2023.4
Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution

Authors: Henrique Botelho Guerra, João F. Ferreira, and João Costa Seco

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Type-directed component-based program synthesis is the task of automatically building a function with applications of available components and whose type matches a given goal type. Existing approaches to component-based synthesis, based on classical proof search, cannot deal with large sets of components. Recently, Hoogle+, a component-based synthesizer for Haskell, overcomes this issue by reducing the search problem to a Petri-net reachability problem. However, Hoogle+ cannot synthesize constants nor λ-abstractions, which limits the problems that it can solve. We present Hoogle⋆, an extension to Hoogle+ that brings constants and λ-abstractions to the search space, in two independent steps. First, we introduce the notion of wildcard component, a component that matches all types. This enables the algorithm to produce incomplete functions, i.e., functions containing occurrences of the wildcard component. Second, we complete those functions, by replacing each occurrence with constants or custom-defined λ-abstractions. We have chosen to find constants by means of an inference algorithm: we present a new unification algorithm based on symbolic execution that uses the input-output examples supplied by the user to compute substitutions for the occurrences of the wildcard. When compared to Hoogle+, Hoogle⋆ can solve more kinds of problems, especially problems that require the generation of constants and λ-abstractions, without performance degradation.
Cite as

Henrique Botelho Guerra, João F. Ferreira, and João Costa Seco. Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 4:1-4:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{botelhoguerra_et_al:LIPIcs.ECOOP.2023.4,
  author =	{Botelho Guerra, Henrique and Ferreira, Jo\~{a}o F. and Costa Seco, Jo\~{a}o},
  title =	{{Hoogle⋆: Constants and \lambda-abstractions in Petri-net-based Synthesis using Symbolic Execution}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{4:1--4:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.4},
  URN =		{urn:nbn:de:0030-drops-181974},
  doi =		{10.4230/LIPIcs.ECOOP.2023.4},
  annote =	{Keywords: Type-directed, component-based, program synthesis, symbolic execution, unification, Haskell}
}
Document
Artifact
DOI: 10.4230/DARTS.9.2.20
Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution (Artifact)

Authors: Henrique Botelho Guerra, João F. Ferreira, and João Costa Seco

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Type-directed component-based program synthesis is the task of automatically building a function with applications of available components and whose type matches a given goal type. Existing approaches to component-based synthesis, based on classical proof search, cannot deal with large sets of components. Recently, Hoogle+, a component-based synthesizer for Haskell, overcomes this issue by reducing the search problem to a Petri-net reachability problem. However, Hoogle+ cannot synthesize constants nor λ-abstractions, which limits the problems that it can solve. We present Hoogle⋆, an extension to Hoogle+ that brings constants and λ-abstractions to the search space, in two independent steps. First, we introduce the notion of wildcard component, a component that matches all types. This enables the algorithm to produce incomplete functions, i.e., functions containing occurrences of the wildcard component. Second, we complete those functions, by replacing each occurrence with constants or custom-defined λ-abstractions. We have chosen to find constants by means of an inference algorithm: we present a new unification algorithm based on symbolic execution that uses the input-output examples supplied by the user to compute substitutions for the occurrences of the wildcard. When compared to Hoogle+, Hoogle⋆ can solve more kinds of problems, especially problems that require the generation of constants and λ-abstractions, without performance degradation. The artifact contains the source code of Hoogle⋆, as well as scripts to reproduce the evaluation done in the paper.
Cite as

Henrique Botelho Guerra, João F. Ferreira, and João Costa Seco. Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 20:1-20:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{botelhoguerra_et_al:DARTS.9.2.20,
  author =	{Botelho Guerra, Henrique and Ferreira, Jo\~{a}o F. and Costa Seco, Jo\~{a}o},
  title =	{{Hoogle⋆: Constants and \lambda-abstractions in Petri-net-based Synthesis using Symbolic Execution (Artifact)}},
  pages =	{20:1--20:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Botelho Guerra, Henrique and Ferreira, Jo\~{a}o F. and Costa Seco, Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.20},
  URN =		{urn:nbn:de:0030-drops-182609},
  doi =		{10.4230/DARTS.9.2.20},
  annote =	{Keywords: Type-directed, component-based, program synthesis, symbolic execution, unification, Haskell}
}
  • Refine by Type
  • 5 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 2 2024
  • 2 2023

  • Refine by Author
  • 4 Costa Seco, João
  • 2 Botelho Guerra, Henrique
  • 2 Carvalho, Luís
  • 2 Ferreira, João F.
  • 1 Ferdowsi, Kasra
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs
  • 2 DARTS

  • Refine by Classification
  • 3 Software and its engineering → Automatic programming
  • 2 Theory of computation → Automated reasoning
  • 2 Theory of computation → Program semantics
  • 2 Theory of computation → Type theory

  • Refine by Keyword
  • 2 Haskell
  • 2 Software evolution
  • 2 Type-directed
  • 2 component-based
  • 2 program synthesis
  • 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