Caros, O Grupo de Estruturas Formais, Fundamentos e Aplicações (EFFA <http://inf.ufg.br/~daniel/effa/>/UFG), em associação ao Grupo de Teoria da Computação (GTC <http://ayala.mat.unb.br/TCgroup/index.html/>/UnB), convida-os à participação do seminário remoto <https://sites.google.com/view/gtc-unb/calendar> 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 <https://www.irif.fr/~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. *Data: *02 de outubro de 2020 (sexta-feira) *Horário: *10.00h *Link: *https://meet.google.com/nhv-smko-aot -- 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/CAGA4ea9Z_R9OYhv8Q0rLqgSaia7YSthRrVPOBUPZmzOd-s_W8Q%40mail.gmail.com.
