Mathematical Logic Seminar

Reasoning about Choreographic Programs

Sala 6.2.33, Ciências ULisboa (com transmissão online)

Por Luís Cruz-Filipe (University of Southern Denmark).

Choreographic programming is a paradigm where a concurrent or distributed system is developed in a top-down fashion. Programs, called choreographies, detail the desired interactions between processes, and can be compiled to distributed implementations based on message passing. Choreographic languages usually guarantee deadlock-freedom and provide an operational correspondence between choreographies and their compiled implementations, but until now little work has been done on verifying other properties.

This talk presents a Hoare-style logic for reasoning about the behaviour of choreographies, and illustrate its usage in representative examples. We show that this logic is sound and complete, and discuss decidability of its judgements. Using existing results from choreographic programming, we show that {any functional correctness property proven for a choreography also holds for its} compiled implementation.


Transmissão via Zoom.

16h00
CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional
Titulo e data do evento, com imagem de ponte sobre o tejo

Um evento organizado no âmbito da Ação COST EURO-MIC, de cujo Comitê de Gestão Elisabete Silva, líder do Bioactive and Multifunctional Materials Lab do BioISI, faz parte.

Logótipo do EVM 2024

Por: Jorge Buescu (DM Ciências ULisboa e CMAFcIO).

Logótipo do EVM 2024

Por Jean-Baptiste Casteras (DM Ciências ULisboa e CMAFcIO).

Chegou a hora: os participantes do Programa Ser Cientista vão apresentar os projetos que desenvolveram ao longo de uma semana, acompanhados por docentes e investigadores de CIÊNCIAS. E todos podem assistir!

Imagem do evento

Extended enrolement date until July 12th.

Logótipo do evento, sobre um fundo branco

Um evento de reunião da comunidade nacional nas diversas vertentes da informática, com a ambição de ser o fórum de eleição para a divulgação, discussão e reconhecimento de trabalhos científicos.

Are you ready for this year's edition?

Imagem do evento - título, local e data do evento

Investigação Ecológica ao Serviço da Conservação

A leading venue for presenting and discussing the latest research, industrial practice and innovations in dependable and secure computing.