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.
Attempts at Improvement
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 |
|---|---|---|---|---|
MANUNKIND: Determinants and Dynamics of Collaborative ExploitationThis project aims to develop a game theoretic framework to analyze the psychological and strategic dynamics of collaborative exploitation, informing policies to combat modern slavery. | ERC STG | € 1.497.749 | 2022 | Details |
Elucidating the phenotypic convergence of proliferation reduction under growth-induced pressureThe UnderPressure project aims to investigate how mechanical constraints from 3D crowding affect cell proliferation and signaling in various organisms, with potential applications in reducing cancer chemoresistance. | ERC STG | € 1.498.280 | 2022 | Details |
The Ethics of Loneliness and SociabilityThis project aims to develop a normative theory of loneliness by analyzing ethical responsibilities of individuals and societies to prevent and alleviate loneliness, establishing a new philosophical sub-field. | ERC STG | € 1.025.860 | 2023 | Details |
Uncovering the mechanisms of action of an antiviral bacteriumThis project aims to uncover the mechanisms behind Wolbachia's antiviral protection in insects and develop tools for studying symbiont gene function. | ERC STG | € 1.500.000 | 2023 | Details |
MANUNKIND: Determinants and Dynamics of Collaborative Exploitation
This project aims to develop a game theoretic framework to analyze the psychological and strategic dynamics of collaborative exploitation, informing policies to combat modern slavery.
Elucidating the phenotypic convergence of proliferation reduction under growth-induced pressure
The UnderPressure project aims to investigate how mechanical constraints from 3D crowding affect cell proliferation and signaling in various organisms, with potential applications in reducing cancer chemoresistance.
The Ethics of Loneliness and Sociability
This project aims to develop a normative theory of loneliness by analyzing ethical responsibilities of individuals and societies to prevent and alleviate loneliness, establishing a new philosophical sub-field.
Uncovering the mechanisms of action of an antiviral bacterium
This project aims to uncover the mechanisms behind Wolbachia's antiviral protection in insects and develop tools for studying symbiont gene function.
Vergelijkbare projecten uit andere regelingen
| Project | Regeling | Bedrag | Jaar | Actie |
|---|---|---|---|---|
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 STG | € 1.482.690 | 2022 | Details |
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 ADG | € 2.470.023 | 2023 | Details |
Program Intelligence, Declaratively and SymbolicallyThe PINDESYM project aims to advance automatic program understanding by integrating symbolic reasoning and machine learning into a unified declarative analysis framework. | ERC ADG | € 2.395.875 | 2024 | Details |
Exploratory Program SynthesisDeveloping Exploratory Program Synthesis tools to enhance productivity and reliability in coding by enabling code generation even with incomplete specifications. | ERC STG | € 1.500.000 | 2023 | Details |
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.
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.
Program Intelligence, Declaratively and Symbolically
The PINDESYM project aims to advance automatic program understanding by integrating symbolic reasoning and machine learning into a unified declarative analysis framework.
Exploratory Program Synthesis
Developing Exploratory Program Synthesis tools to enhance productivity and reliability in coding by enabling code generation even with incomplete specifications.