15 Search Results for "Cruz-Filipe, Luís"

Volume

OASIcs, Volume 78

Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)

Microservices 2017/2019, February 19-21, 2019, University of Applied Sciences and Arts Dortmund, Germany

Editors: Luís Cruz-Filipe, Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, Florian Rademacher, and Sabine Sachweh

Document
DOI: 10.4230/LIPIcs.ITP.2026.15
Formalizing a Hoare Calculus for Choreographic Programming

Authors: Luís Cruz-Filipe and Thomas Wulff Heissel

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distributed implementation is compiled automatically. Choreographies formalize the way many practitioners think about distributed protocols, and are a natural framework in which to prove properties of such protocols. Previous work has introduced a Hoare calculus for reasoning about choreographies. In this article, we show how a formalization of that work in a theorem prover revealed several issues with the pen-and-paper development. We discuss the extent to which these issues can be fixed, and conclude with some considerations on the need for more formal verification of research results.
Cite as

Luís Cruz-Filipe and Thomas Wulff Heissel. Formalizing a Hoare Calculus for Choreographic Programming. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{cruzfilipe_et_al:LIPIcs.ITP.2026.15,
  author =	{Cruz-Filipe, Lu{\'\i}s and Heissel, Thomas Wulff},
  title =	{{Formalizing a Hoare Calculus for Choreographic Programming}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.15},
  URN =		{urn:nbn:de:0030-drops-269896},
  doi =		{10.4230/LIPIcs.ITP.2026.15},
  annote =	{Keywords: choreographic programming, theorem proving, Hoare calculus}
}
Document
Invited Paper
DOI: 10.4230/OASIcs.RW.2024/2025.5
Inconsistency-Tolerant Semantics Based on (Preferred) Repairs (Invited Paper)

Authors: Camille Bourgaux

Published in: OASIcs, Volume 138, Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025)

Abstract
Real-world datasets are plagued by data quality issues which may render the data inconsistent w.r.t. a set of constraints, be they given by database integrity constraints or ontologies. A prominent way to handle such inconsistent data is to use inconsistency-tolerant semantics to obtain meaningful answers to queries. Most of these semantics are based on some notion of repairs, which represent ways of restoring the data consistency. The most basic kind of repairs is that of subset repairs, which are maximal consistent subsets of the dataset. However, in many scenarios, one can define preferred repairs based on some preference information. These lecture notes present inconsistency-tolerant semantics, focusing on the repair-based ones, then review different kinds of preferred repairs that have been considered in the literature. We present in particular the relationships between different kinds of preferred repairs and other notions related to inconsistency handling, the computational complexity of reasoning with (preferred) repairs, and some implementations.
Cite as

Camille Bourgaux. Inconsistency-Tolerant Semantics Based on (Preferred) Repairs (Invited Paper). In Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025). Open Access Series in Informatics (OASIcs), Volume 138, pp. 5:1-5:67, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bourgaux:OASIcs.RW.2024/2025.5,
  author =	{Bourgaux, Camille},
  title =	{{Inconsistency-Tolerant Semantics Based on (Preferred) Repairs}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{5:1--5:67},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-405-5},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{138},
  editor =	{Artale, Alessandro and Bienvenu, Meghyn and Garc{\'\i}a, Yazm{\'\i}n Ib\'{a}\~{n}ez and Murlak, Filip},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.RW.2024/2025.5},
  URN =		{urn:nbn:de:0030-drops-250504},
  doi =		{10.4230/OASIcs.RW.2024/2025.5},
  annote =	{Keywords: Knowledge bases, databases, inconsistency handling, repairs, preferences}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.26
Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL

Authors: Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark Barrett, and Cesare Tinelli

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

Abstract
Sledgehammer is a tool that increases the level of automation in the Isabelle/HOL proof assistant by asking external automatic theorem provers (ATPs), including SMT solvers, to prove the current goal. When the external ATP succeeds it must provide enough evidence that the goal holds for Isabelle to be able to reprove it internally based on that evidence. In particular, Isabelle can do this by replaying fine-grained proof certificates from proof-producing SMT solvers as long as they are expressed in the Alethe format, which until now was supported only by the veriT SMT solver. We report on our experience adding proof reconstruction support for the cvc5 SMT solver in Isabelle by extending cvc5 to produce proofs in the Alethe format and then adapting Isabelle to reconstruct those proofs. We discuss several difficulties and pitfalls we encountered and describe a set of tools and techniques we developed to improve the process. A notable outcome of this effort is that Isabelle can now be used as an independent proof checker for SMT problems written in the SMT-LIB standard. We evaluate cvc5’s integration on a set of SMT-LIB benchmarks originating from Isabelle as well as on a set of Isabelle proofs. Our results confirm that this integration complements and improves Sledgehammer’s capabilities.
Cite as

Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark Barrett, and Cesare Tinelli. Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lachnitt_et_al:LIPIcs.ITP.2025.26,
  author =	{Lachnitt, Hanna and Fleury, Mathias and Barbosa, Haniel and Jakpor, Jibiana and Andreotti, Bruno and Reynolds, Andrew and Schurr, Hans-J\"{o}rg and Barrett, Clark and Tinelli, Cesare},
  title =	{{Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{26:1--26:22},
  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.26},
  URN =		{urn:nbn:de:0030-drops-246243},
  doi =		{10.4230/LIPIcs.ITP.2025.26},
  annote =	{Keywords: interactive theorem proving, proof assistants, Isabelle/HOL, SMT, certification, proof certificates, proof reconstruction, proof automation}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.15
Certified Implementability of Global Multiparty Protocols

Authors: Elaine Li and Thomas Wies

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

Abstract
Implementability is the decision problem at the heart of top-down approaches to protocol verification. In this paper, we present a mechanization of a recently proposed precise implementability characterization by Li et al. for a large class of protocols that subsumes many existing formalisms in the literature. Our protocols and implementations model asynchronous commmunication, and can exhibit infinite behavior. We improve upon their pen-and-paper results by unifying distinct formalisms, simplifying existing proof arguments, elaborating on the construction of canonical implementations, and even uncovering a subtle bug in the semantics for infinite words. As a corollary of our mechanization, we show that the original characterization of implementability applies even to protocols with infinitely many participants. We also contribute a reusable library for reasoning about generic communicating state machines. Our mechanization consists of about 15k lines of Rocq code. We believe that our mechanization can provide the foundation for deductively proving the implementability of protocols beyond the reach of prior work, extracting certified implementations for finite protocols, and investigating implementability under alternative asynchronous communication models.
Cite as

Elaine Li and Thomas Wies. Certified Implementability of Global Multiparty Protocols. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 15:1-15:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.ITP.2025.15,
  author =	{Li, Elaine and Wies, Thomas},
  title =	{{Certified Implementability of Global Multiparty Protocols}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{15:1--15:20},
  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.15},
  URN =		{urn:nbn:de:0030-drops-246139},
  doi =		{10.4230/LIPIcs.ITP.2025.15},
  annote =	{Keywords: Asynchronous protocols, communicating state machines, labeled transition systems, infinite semantics, realizability, multiparty session types, choreographies, deadlock freedom}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.21
Practically Feasible Proof Logging for Pseudo-Boolean Optimization

Authors: Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, and Marc Vinyals

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Certifying solvers have long been standard for decision problems in Boolean satisfiability (SAT), allowing for proof logging and checking with very limited overhead, but developing similar tools for combinatorial optimization has remained a challenge. A recent promising approach covering a wide range of solving paradigms is pseudo-Boolean proof logging, but this has mostly consisted of proof-of-concept works far from delivering the performance required for real-world deployment. In this work, we present an efficient toolchain based on VeriPB and CakePB for formally verified pseudo-Boolean optimization. We implement proof logging for the full range of techniques in the state-of-the-art solvers RoundingSat and Sat4j, including core-guided search and linear programming integration with Farkas certificates and cut generation. Our experimental evaluation shows that proof logging and checking performance in this much more expressive paradigm is now quite close to the level of SAT solving, and hence is clearly practically feasible.
Cite as

Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, and Marc Vinyals. Practically Feasible Proof Logging for Pseudo-Boolean Optimization. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 21:1-21:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{koops_et_al:LIPIcs.CP.2025.21,
  author =	{Koops, Wietze and Le Berre, Daniel and Myreen, Magnus O. and Nordstr\"{o}m, Jakob and Oertel, Andy and Tan, Yong Kiam and Vinyals, Marc},
  title =	{{Practically Feasible Proof Logging for Pseudo-Boolean Optimization}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{21:1--21:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.21},
  URN =		{urn:nbn:de:0030-drops-238825},
  doi =		{10.4230/LIPIcs.CP.2025.21},
  annote =	{Keywords: proof logging, certifying algorithms, combinatorial optimization, certification, pseudo-Boolean solving, 0-1 integer linear programming}
}
Document
DOI: 10.4230/OASIcs.Microservices.2020-2022.3
Modular Choreographies: Bridging Alice and Bob Notation to Java

Authors: Luís Cruz-Filipe, Anne Madsen, Fabrizio Montesi, and Marco Peressotti

Published in: OASIcs, Volume 111, Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)

Abstract
We present Modular Choreographies, a new choreographic programming language that features modular functions. Modular Choreographies is aimed at simplicity: its communication abstraction follows the simple tradition from the "Alice and Bob" notation. We develop a compiler toolchain that translates choreographies into modular Java libraries, which developers can use to participate correctly in choreographies. The key novelty is to compile through the Choral language, which was previously proposed to define object-oriented choreographies: our toolchain compiles Modular Choreographies to Choral, and then leverages the existing Choral compiler to generate Java code. Our work is the first to bridge the simplicity of traditional choreographic programming languages with the requirement of generating modular libraries in a mainstream language (Java).
Cite as

Luís Cruz-Filipe, Anne Madsen, Fabrizio Montesi, and Marco Peressotti. Modular Choreographies: Bridging Alice and Bob Notation to Java. In Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022). Open Access Series in Informatics (OASIcs), Volume 111, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{cruzfilipe_et_al:OASIcs.Microservices.2020-2022.3,
  author =	{Cruz-Filipe, Lu{\'\i}s and Madsen, Anne and Montesi, Fabrizio and Peressotti, Marco},
  title =	{{Modular Choreographies: Bridging Alice and Bob Notation to Java}},
  booktitle =	{Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)},
  pages =	{3:1--3:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-306-5},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{111},
  editor =	{Dorai, Gokila and Gabbrielli, Maurizio and Manzonetto, Giulio and Osmani, Aomar and Prandini, Marco and Zavattaro, Gianluigi and Zimmermann, Olaf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2020-2022.3},
  URN =		{urn:nbn:de:0030-drops-194650},
  doi =		{10.4230/OASIcs.Microservices.2020-2022.3},
  annote =	{Keywords: Choreographic Programming, Choreographies, Modularity}
}
Document
Survey
DOI: 10.4230/TGDK.1.1.11
How Does Knowledge Evolve in Open Knowledge Graphs?

Authors: Axel Polleres, Romana Pernisch, Angela Bonifati, Daniele Dell'Aglio, Daniil Dobriy, Stefania Dumbrava, Lorena Etcheverry, Nicolas Ferranti, Katja Hose, Ernesto Jiménez-Ruiz, Matteo Lissandrini, Ansgar Scherp, Riccardo Tommasini, and Johannes Wachs

Published in: TGDK, Volume 1, Issue 1 (2023): Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge, Volume 1, Issue 1

Abstract
Openly available, collaboratively edited Knowledge Graphs (KGs) are key platforms for the collective management of evolving knowledge. The present work aims t o provide an analysis of the obstacles related to investigating and processing specifically this central aspect of evolution in KGs. To this end, we discuss (i) the dimensions of evolution in KGs, (ii) the observability of evolution in existing, open, collaboratively constructed Knowledge Graphs over time, and (iii) possible metrics to analyse this evolution. We provide an overview of relevant state-of-the-art research, ranging from metrics developed for Knowledge Graphs specifically to potential methods from related fields such as network science. Additionally, we discuss technical approaches - and their current limitations - related to storing, analysing and processing large and evolving KGs in terms of handling typical KG downstream tasks.
Cite as

Axel Polleres, Romana Pernisch, Angela Bonifati, Daniele Dell'Aglio, Daniil Dobriy, Stefania Dumbrava, Lorena Etcheverry, Nicolas Ferranti, Katja Hose, Ernesto Jiménez-Ruiz, Matteo Lissandrini, Ansgar Scherp, Riccardo Tommasini, and Johannes Wachs. How Does Knowledge Evolve in Open Knowledge Graphs?. In Special Issue on Trends in Graph Data and Knowledge. Transactions on Graph Data and Knowledge (TGDK), Volume 1, Issue 1, pp. 11:1-11:59, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{polleres_et_al:TGDK.1.1.11,
  author =	{Polleres, Axel and Pernisch, Romana and Bonifati, Angela and Dell'Aglio, Daniele and Dobriy, Daniil and Dumbrava, Stefania and Etcheverry, Lorena and Ferranti, Nicolas and Hose, Katja and Jim\'{e}nez-Ruiz, Ernesto and Lissandrini, Matteo and Scherp, Ansgar and Tommasini, Riccardo and Wachs, Johannes},
  title =	{{How Does Knowledge Evolve in Open Knowledge Graphs?}},
  journal =	{Transactions on Graph Data and Knowledge},
  pages =	{11:1--11:59},
  year =	{2023},
  volume =	{1},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/TGDK.1.1.11},
  URN =		{urn:nbn:de:0030-drops-194855},
  doi =		{10.4230/TGDK.1.1.11},
  annote =	{Keywords: KG evolution, temporal KG, versioned KG, dynamic KG}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.11
Now It Compiles! Certified Automatic Repair of Uncompilable Protocols

Authors: Luís Cruz-Filipe and Fabrizio Montesi

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distributed implementation is compiled automatically. Unfortunately, it is possible to write choreographies that cannot be compiled, because of issues related to an agreement property known as knowledge of choice. This forces programmers to reason manually about implementation details that may be orthogonal to the protocol that they are writing. Amendment is an automatic procedure for repairing uncompilable choreographies. We present a formalisation of amendment from the literature, built upon an existing formalisation of choreographic programming. However, in the process of formalising the expected properties of this procedure, we discovered a subtle counterexample that invalidates the original published and peer-reviewed pen-and-paper theory. We discuss how using a theorem prover led us to both finding the issue, and stating and proving a correct formulation of the properties of amendment.
Cite as

Luís Cruz-Filipe and Fabrizio Montesi. Now It Compiles! Certified Automatic Repair of Uncompilable Protocols. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{cruzfilipe_et_al:LIPIcs.ITP.2023.11,
  author =	{Cruz-Filipe, Lu{\'\i}s and Montesi, Fabrizio},
  title =	{{Now It Compiles! Certified Automatic Repair of Uncompilable Protocols}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.11},
  URN =		{urn:nbn:de:0030-drops-183867},
  doi =		{10.4230/LIPIcs.ITP.2023.11},
  annote =	{Keywords: choreographic programming, theorem proving, compilation, program repair}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2023.7
Modular Compilation for Higher-Order Functional Choreographies

Authors: Luís Cruz-Filipe, Eva Graversen, Lovro Lugović, Fabrizio Montesi, and Marco Peressotti

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

Abstract
Choreographic programming is a paradigm for concurrent and distributed software, whereby descriptions of the intended communications (choreographies) are automatically compiled into distributed code with strong safety and liveness properties (e.g., deadlock-freedom). Recent efforts tried to combine the theories of choreographic programming and higher-order functional programming, in order to integrate the benefits of the former with the modularity of the latter. However, they do not offer a satisfactory theory of compilation compared to the literature, because of important syntactic and semantic shortcomings: compilation is not modular (editing a part might require recompiling everything) and the generated code can perform unexpected global synchronisations. In this paper, we find that these shortcomings are not mere coincidences. Rather, they stem from genuine new challenges posed by the integration of choreographies and functions: knowing which participants are involved in a choreography becomes nontrivial, and divergence in applications requires rethinking how to prove the semantic correctness of compilation. We present a novel theory of compilation for functional choreographies that overcomes these challenges, based on types and a careful design of the semantics of choreographies and distributed code. The result: a modular notion of compilation, which produces code that is deadlock-free and correct (it operationally corresponds to its source choreography).
Cite as

Luís Cruz-Filipe, Eva Graversen, Lovro Lugović, Fabrizio Montesi, and Marco Peressotti. Modular Compilation for Higher-Order Functional Choreographies. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 7:1-7:37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{cruzfilipe_et_al:LIPIcs.ECOOP.2023.7,
  author =	{Cruz-Filipe, Lu{\'\i}s and Graversen, Eva and Lugovi\'{c}, Lovro and Montesi, Fabrizio and Peressotti, Marco},
  title =	{{Modular Compilation for Higher-Order Functional Choreographies}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{7:1--7:37},
  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.7},
  URN =		{urn:nbn:de:0030-drops-182005},
  doi =		{10.4230/LIPIcs.ECOOP.2023.7},
  annote =	{Keywords: Choreographies, Concurrency, \lambda-calculus, Type Systems}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.15
Formalising a Turing-Complete Choreographic Language in Coq

Authors: Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti

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

Abstract
The theory of choreographic languages typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of them lead to long reviewing processes, and occasionally to errors being found in published proofs. In this work, we take a published proof of Turing completeness of a choreographic language and formalise it in Coq. Our development includes formalising the choreographic language, its basic properties, Kleene’s theory of partial recursive functions, the encoding of these functions as choreographies, and a proof that this encoding is correct. With this effort, we show that theorem proving can be a very useful tool in the field of choreographic languages: besides the added degree of confidence that we get from a mechanised proof, the formalisation process led us to a significant simplification of the underlying theory. Our results offer a foundation for the future formal development of choreographic languages.
Cite as

Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. Formalising a Turing-Complete Choreographic Language in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{cruzfilipe_et_al:LIPIcs.ITP.2021.15,
  author =	{Cruz-Filipe, Lu{\'\i}s and Montesi, Fabrizio and Peressotti, Marco},
  title =	{{Formalising a Turing-Complete Choreographic Language in Coq}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{15:1--15:18},
  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.15},
  URN =		{urn:nbn:de:0030-drops-139109},
  doi =		{10.4230/LIPIcs.ITP.2021.15},
  annote =	{Keywords: Choreographic Programming, Formalisation, Turing Completeness}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.5
The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service

Authors: Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Davide Sangiorgi, and Stefano Pio Zingaro

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
Serverless computing is a paradigm for programming cloud applications in terms of stateless functions, executed and scaled in proportion to inbound requests. Here, we revisit SKC, a calculus capturing the essential features of serverless programming. By exploring the design space of the language, we refined the integration between the fundamental features of the two calculi that inspire SKC: the λ- and the π-calculus. That investigation led us to a revised syntax and semantics, which support an increase in the expressiveness of the language. In particular, now function names are first-class citizens and can be passed around. To illustrate the new features, we present step-by-step examples and two non-trivial use cases from artificial intelligence, which model, respectively, a perceptron and an image tagging system into compositions of serverless functions. We also illustrate how SKC supports reasoning on serverless implementations, i.e., the underlying network of communicating, concurrent, and mobile processes which execute serverless functions in the cloud. To that aim, we show an encoding from SKC to the asynchronous π-calculus and prove it correct in terms of an operational correspondence. Dedicated to Maurizio Gabbrielli, on his 60th birthday (... rob da mët ! )
Cite as

Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Davide Sangiorgi, and Stefano Pio Zingaro. The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{giallorenzo_et_al:OASIcs.Gabbrielli.5,
  author =	{Giallorenzo, Saverio and Lanese, Ivan and Montesi, Fabrizio and Sangiorgi, Davide and Zingaro, Stefano Pio},
  title =	{{The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{5:1--5:21},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.5},
  URN =		{urn:nbn:de:0030-drops-132271},
  doi =		{10.4230/OASIcs.Gabbrielli.5},
  annote =	{Keywords: Serverless computing, Process calculi, Pi-calculus}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.Microservices.2017-2019
OASIcs, Volume 78, Microservices 2017/2019, Complete Volume

Authors: Luís Cruz-Filipe, Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, Florian Rademacher, and Sabine Sachweh

Published in: OASIcs, Volume 78, Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)

Abstract
OASIcs, Volume 78, Microservices 2017/2019, Complete Volume
Cite as

Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019). Open Access Series in Informatics (OASIcs), Volume 78, pp. 1-98, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Proceedings{cruzfilipe_et_al:OASIcs.Microservices.2017-2019,
  title =	{{OASIcs, Volume 78, Microservices 2017/2019, Complete Volume}},
  booktitle =	{Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)},
  pages =	{1--98},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-137-5},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{78},
  editor =	{Cruz-Filipe, Lu{\'\i}s and Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian and Sachweh, Sabine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2017-2019},
  URN =		{urn:nbn:de:0030-drops-118301},
  doi =		{10.4230/OASIcs.Microservices.2017-2019},
  annote =	{Keywords: OASIcs, Volume 78, Microservices 2017/2019, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/OASIcs.Microservices.2017-2019.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Luís Cruz-Filipe, Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, Florian Rademacher, and Sabine Sachweh

Published in: OASIcs, Volume 78, Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019). Open Access Series in Informatics (OASIcs), Volume 78, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cruzfilipe_et_al:OASIcs.Microservices.2017-2019.0,
  author =	{Cruz-Filipe, Lu{\'\i}s and Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian and Sachweh, Sabine},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)},
  pages =	{0:i--0:xiv},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-137-5},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{78},
  editor =	{Cruz-Filipe, Lu{\'\i}s and Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian and Sachweh, Sabine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2017-2019.0},
  URN =		{urn:nbn:de:0030-drops-118225},
  doi =		{10.4230/OASIcs.Microservices.2017-2019.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/OASIcs.ICLP.2016.11
Grounded Fixpoints and Active Integrity Constraints

Authors: Luís Cruz-Filipe

Published in: OASIcs, Volume 52, Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016)

Abstract
The formalism of active integrity constraints was introduced as a way to specify particular classes of integrity constraints over relational databases together with preferences on how to repair existing inconsistencies. The rule-based syntax of such integrity constraints also provides algorithms for finding such repairs that achieve the best asymptotic complexity. However, the different semantics that have been proposed for these integrity constraints all exhibit some counter-intuitive examples. In this work, we look at active integrity constraints using ideas from algebraic fixpoint theory. We show how database repairs can be modeled as fixpoints of particular operators on databases, and study how the notion of grounded fixpoint induces a corresponding notion of grounded database repair that captures several natural intuitions, and in particular avoids the problems of previous alternative semantics. In order to study grounded repairs in their full generality, we need to generalize the notion of grounded fixpoint to non-deterministic operators. We propose such a definition and illustrate its plausibility in the database context.
Cite as

Luís Cruz-Filipe. Grounded Fixpoints and Active Integrity Constraints. In Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016). Open Access Series in Informatics (OASIcs), Volume 52, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{cruzfilipe:OASIcs.ICLP.2016.11,
  author =	{Cruz-Filipe, Lu{\'\i}s},
  title =	{{Grounded Fixpoints and Active Integrity Constraints}},
  booktitle =	{Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016)},
  pages =	{11:1--11:14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-007-1},
  ISSN =	{2190-6807},
  year =	{2016},
  volume =	{52},
  editor =	{Carro, Manuel and King, Andy and Saeedloei, Neda and De Vos, Marina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICLP.2016.11},
  URN =		{urn:nbn:de:0030-drops-67411},
  doi =		{10.4230/OASIcs.ICLP.2016.11},
  annote =	{Keywords: grounded fixpoints, active integrity constraints}
}
  • Refine by Type
  • 14 Document/PDF
  • 5 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 1 2026
  • 4 2025
  • 4 2023
  • 1 2021
  • 4 2020
  • Show More...

  • Refine by Author
  • 8 Cruz-Filipe, Luís
  • 7 Montesi, Fabrizio
  • 5 Peressotti, Marco
  • 3 Giallorenzo, Saverio
  • 2 Rademacher, Florian
  • Show More...

  • Refine by Series/Journal
  • 7 LIPIcs
  • 6 OASIcs
  • 1 TGDK

  • Refine by Classification
  • 4 Theory of computation → Automated reasoning
  • 3 Applied computing → Service-oriented architectures
  • 3 Theory of computation → Concurrency
  • 3 Theory of computation → Distributed computing models
  • 3 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 2 Choreographic Programming
  • 2 Choreographies
  • 2 certification
  • 2 choreographic programming
  • 2 theorem proving
  • 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