Caros, o Grupo de Teoria da Computação da UnB (GTC-UNB) em associação ao Grupo de Estruturas Formais, Fundamentos e Aplicações (EFFA <http://www.google.com/url?q=http%3A%2F%2Finf.ufg.br%2F~daniel%2Feffa%2F&sa=D&sntz=1&usg=AFQjCNGBb6kpjwQQpby5p-lZ8XRo_nc3IQ>/UFG), convida-os à participação do seminário remoto do grupos de pesquisa em temas relacionados aos Fundamentos em Computação e Matemática. Os seminários ocorrem às sextas-feiras, 10:00 (horário de Brasília).
O seminário da próxima sexta, dia 25/09, ás 10:00, será proferido pelo Prof. Jorge Pérez, da Universidade de Groningen, os dados estão abaixo. ------------------------------------------------------------------------------------ * Domain-Aware Session Types* Prof. Jorge Pérez (RUG) (joint work with Luis Caires, Frank Pfenning, and Bernardo Toninho) * Abstract: *We develop a generalization of existing Curry-Howard interpretations of (binary) session types by relying on an extension of linear logic with features from hybrid logic, in particular modal worlds that indicate domains. These worlds govern domain migration, subject to a parametric accessibility relation familiar from the Kripke semantics of modal logic. The result is an expressive new typed process framework for domain-aware, message-passing concurrency. Its logical foundations ensure that well-typed processes enjoy session fidelity, global progress, and termination. Typing also ensures that processes only communicate with accessible domains and so respect the accessibility relation. Remarkably, our domain-aware framework can specify scenarios in which domain information is available only at runtime; flexible accessibility relations can be cleanly defined and statically enforced. As a specific application, we introduce domain-aware multiparty session types, in which global protocols can express arbitrarily nested sub-protocols via domain migration. We develop a precise analysis of these multiparty protocols by reduction to our binary domain-aware framework: complex domain-aware protocols can be reasoned about at the right level of abstraction, ensuring also the principled transfer of key correctness properties from the binary to the multiparty setting. ---------------------------------------- Apresentação poderá ser acessada via link: Join Zoom Meeting https://us02web.zoom.us/j/86258333778?pwd=RHA2WkdKQmpZZUZaMmVaTTZvOUdFUT09 <https://www.google.com/url?q=https://us02web.zoom.us/j/86258333778?pwd%3DRHA2WkdKQmpZZUZaMmVaTTZvOUdFUT09&sa=D&source=calendar&usd=2&usg=AOvVaw3L1Yno_XeY15TkOPJPRfcG> Meeting ID: 862 5833 3778 Passcode: 790028 -- Daniele Nantes Grupo de Teoria da Computação Departamentos de Matemática e Computação Universidade de Brasília www.mat.unb.br/~dnantes -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAMnPOrpKKLwJE1b2jvKEtNUXmZzBH8EM9b4PYCbLfpTrYcHU-w%40mail.gmail.com.
