[convite] Seminário de Teoria da Computação (GTC-UnB + EFFA/UFG)
33 views
Skip to first unread message
Daniele Nantes
Sep 21, 2020, 2:17:01 PM9/21/20
to logi...@dimap.ufrn.br
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/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.
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 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
Daniel Ventura
Sep 28, 2020, 12:11:02 PM9/28/20
to logi...@dimap.ufrn.br
Caros,
O Grupo de Estruturas Formais, Fundamentos e Aplicações (EFFA/UFG), em associação ao Grupo de Teoria da Computação (GTC/UnB), convida-os à participação do seminário remoto dos grupos de pesquisa em temas relacionados aos Fundamentos em Computação e Matemática Aplicada à Computação.
Os seminários ocorrem às sextas-feiras, 10:00 (horário de Brasília).
A palestra nesta sexta - dia 02/10 às 10:00 - será proferida pela Profa. Delia Kesner (Univ. de Paris, CNRS, IRIF). Mais informações abaixo.
at.te
Daniel Ventura
-----------------------------------------------------------------------------------------------------------
Título: Call-by-Push-Value Revisited
Palestrante: Delia Kesner (Université de Paris, CNRS, IRIF;
Institut Universitaire de France)
Resumo:
Call-by-Push-Value (CBPV) is a programming paradigm subsuming both
Call-by-Name (CBN) and Call-by-Value (CBV) semantics. The paradigm was
recently modelled by means of the Bang Calculus, a term language
connecting CBPV and Linear Logic.
This talk presents a revisited version of the Bang Calculus, called lambda!, enjoying some important properties missing in the original system. Indeed, the new calculus integrates commutative conversions to unblock value redexes while being confluent at the same time. The second contribution is related to non-idempotent types. We provide a quantitative type system for the lambda!-calculus, and we show that the length of the (weak) reduction of a typed term to its normal form plus the size of this normal form is bounded by the size of its type derivation. We also explore the properties of this type system with respect to CBN/CBV translations. We keep the original CBN translation from lambda-calculus to the Bang Calculus, which preserves normal forms and is sound and complete with respect to the (quantitative) type system for CBN. However, in the case of CBV, we reformulate both the translation and the type system to restore two main properties: preservation of normal forms and completeness. Last but not least, the quantitative system is refined to a tight one, which transforms the previous upper bound on the length of reduction to normal form plus its size into two independent exact measures for them.
This talk presents a revisited version of the Bang Calculus, called lambda!, enjoying some important properties missing in the original system. Indeed, the new calculus integrates commutative conversions to unblock value redexes while being confluent at the same time. The second contribution is related to non-idempotent types. We provide a quantitative type system for the lambda!-calculus, and we show that the length of the (weak) reduction of a typed term to its normal form plus the size of this normal form is bounded by the size of its type derivation. We also explore the properties of this type system with respect to CBN/CBV translations. We keep the original CBN translation from lambda-calculus to the Bang Calculus, which preserves normal forms and is sound and complete with respect to the (quantitative) type system for CBN. However, in the case of CBV, we reformulate both the translation and the type system to restore two main properties: preservation of normal forms and completeness. Last but not least, the quantitative system is refined to a tight one, which transforms the previous upper bound on the length of reduction to normal form plus its size into two independent exact measures for them.
Reply all
Reply to author
Forward
0 new messages