SubsidieMeestersChoreographies for Distributed Systems: Reasoning, Expressivity, and Development
This project aims to enhance choreographic programming by developing new constructs, verification logics, and a toolchain for effective compilation and deployment of distributed applications.
Projectdetails
Introduction
Decades of research in computing led to high-level programming languages that can turn a programmer's ideas into executable software. For applications that run in isolation, we have a solid toolbox. We can write code with abstract concepts like functions and objects, and then a compiler tool can automatically produce working implementations. This significantly increases productivity, facilitates program analysis, and reduces the risk of bugs.
The Challenge of Distributed Systems
Today, society increasingly relies on distributed systems for work, services, social participation, and so forth. Here, the key high-level concept is that of communication: a message exchange between independent programs. Yet it is nowhere to be found in the syntax of modern programming languages.
Instead, we manually write lower-level instructions for sending and receiving messages in separate programs, hoping that they match each other during execution and produce the wished communications. This is infamously hard, leaving us with code that is difficult to write or trust.
Previous Attempts
This situation is not due to a lack of trying. Choreographic programming is a recent attempt at a programming paradigm with high-level abstractions for communications and their composition in programs called choreographies. Unfortunately, compiling choreographies is technically challenging, which resulted in excessive simplification.
Current theories make unrealistic assumptions, remaining confined to toy scenarios, and reasoning methods for choreographies are underdeveloped.
Project Goals
This project will break new ground by developing:
- New linguistic constructs for choreographies that can deal with realistic scenarios.
- Logics for verifying properties about choreographies and understanding what they mean for the compiled code.
- A toolchain for compiling, testing, and deploying software based on our choreographies.
These actions have the potential to significantly impact how we will model and program distributed applications in the future.
Financiële details & Tijdlijn
Financiële details
| Subsidiebedrag | € 1.999.498 |
| Totale projectbegroting | € 1.999.498 |
Tijdlijn
| Startdatum | 1-6-2024 |
| Einddatum | 31-5-2029 |
| Subsidiejaar | 2024 |
Partners & Locaties
Projectpartners
- SYDDANSK UNIVERSITETpenvoerder
Land(en)
Vergelijkbare projecten binnen European Research Council
| Project | Regeling | Bedrag | Jaar | Actie |
|---|---|---|---|---|
Compositional Higher-Order Reasoning about Distributed SystemsCHORDS aims to develop new theories and methods for compositional verification of distributed systems to enhance software correctness and security through rigorous mathematical reasoning. | ERC Advanced... | € 2.470.023 | 2023 | Details |
A Deductive Verifier for Probabilistic ProgramsThe project aims to commercialize a novel deductive verifier for probabilistic programs by integrating invariant synthesis and program slicing, targeting users and conducting market analysis. | ERC Proof of... | € 150.000 | 2024 | Details |
Formalised Reasoning about Expectations: Composable, Automated, Speedy, TrustworthyFoRECAST aims to develop theoretical foundations and tools for composable automatic differentiation and Bayesian inference, enhancing probabilistic programming for complex modeling applications. | ERC Starting... | € 1.500.000 | 2025 | Details |
Next Generation Laconic CryptographyThis project aims to enhance laconic cryptography by developing efficient protocols and tools to minimize communication complexity while addressing existing inefficiencies and assumptions. | ERC Starting... | € 1.482.690 | 2022 | Details |
Logic and Automata over Sequences with DataThe project aims to overcome undecidability in automata theory over infinite alphabets by developing new decidable models and algorithms for analyzing data languages, with applications in graph databases, program verification, and machine learning. | ERC Consolid... | € 1.998.956 | 2023 | Details |
Compositional Higher-Order Reasoning about Distributed Systems
CHORDS aims to develop new theories and methods for compositional verification of distributed systems to enhance software correctness and security through rigorous mathematical reasoning.
A Deductive Verifier for Probabilistic Programs
The project aims to commercialize a novel deductive verifier for probabilistic programs by integrating invariant synthesis and program slicing, targeting users and conducting market analysis.
Formalised Reasoning about Expectations: Composable, Automated, Speedy, Trustworthy
FoRECAST aims to develop theoretical foundations and tools for composable automatic differentiation and Bayesian inference, enhancing probabilistic programming for complex modeling applications.
Next Generation Laconic Cryptography
This project aims to enhance laconic cryptography by developing efficient protocols and tools to minimize communication complexity while addressing existing inefficiencies and assumptions.
Logic and Automata over Sequences with Data
The project aims to overcome undecidability in automata theory over infinite alphabets by developing new decidable models and algorithms for analyzing data languages, with applications in graph databases, program verification, and machine learning.
Vergelijkbare projecten uit andere regelingen
| Project | Regeling | Bedrag | Jaar | Actie |
|---|---|---|---|---|
DNA-based Infrastructure for Storage and ComputationThe DISCO project aims to engineer a robust DNA-based storage and computing platform, starting with a 10-bit prototype and scaling to hundreds of bits using advanced molecular techniques. | EIC Pathfinder | € 3.993.665 | 2023 | Details |
DNA-based Infrastructure for Storage and Computation
The DISCO project aims to engineer a robust DNA-based storage and computing platform, starting with a 10-bit prototype and scaling to hundreds of bits using advanced molecular techniques.