Temur Kutsia

Johannes Kepler University Linz

Abstract: Proximity relations are binary fuzzy relations that satisfy reflexivity and symmetry properties but are not transitive. They induce the notion of distance between function symbols, which is further extended to terms. In this context, the notion of equality between terms is replaced by "sufficient closeness". We consider three fundamental symbolic computation problems for proximity relations: unification, matching, and anti-unification, present algorithms to solve them, and discuss their properties.

Horário: 10:30 (UTC-3)

Profa. Giselle Reis

Carnegie Mellon University (CMU-Qatar)

Abstract: We look into the problem of unifying multisets containing (first-order) terms and multiple multiset variables. The variables are labelled, meaning that a unifier that places a term in a multiset variable Mi is different from another that places a term in a multiset variable Mj, for i \neq j. We describe a sound, complete, and terminating algorithm for computing the set of all possible unifiers, and analyse its complexity. We also prove an input pre-processing step that avoids the computation of less general unifiers.

Horário: 10:30 (UTC-3)

Joseph Paulus (PhD student)

University of Groningen

Abstract: Encodings of the Lambda-Calculus into the Pi-Calculus have long revealed a fundamental insight: how communication in the Pi-Calculus subsumes evaluation in the Lambda-Calculus. We extend this important line of work by focusing on how such encodings can precisely account for non-determinism and failures in computations, with the aid of types.

On the sequential side, we consider the Resource Calculus, a non-deterministic functional calculus in which intersection types control resources; on the concurrent side, we consider the session Pi-Calculus, in which non-determinism and failure are elegantly supported by the Curry-Howard correspondence that connects linear logic and session types.

We develop two encodings from Resource Calculus into the session Pi-Calculus and establish their correctness: while the first encoding considers failure-free computation, the second goes beyond to explain how failures in Resource Calculus (absence or excess of resources) can be faithfully represented as typed processes in the session Pi-Calculus .

Horário: 10:00 (UTC-3)

Profa. Elaine Pimentel

DMAT/UFRN

Abstract: We look at substructural calculi from a game semantic point of view, guided by certain intuitions about resource conscious and, more specifically, cost conscious reasoning. To this aim, we start with a game, where player I defends a claim corresponding to a (single-conclusion) sequent, while player II tries to refute that claim. Branching rules for additive connectives are modeled by choices of II, while branching for multiplicative connectives leads to splitting the game into parallel subgames, all of which have to be won by player I to succeed. The game comes into full swing by adding cost labels to assumptions, and a corresponding budget. Different proofs of the same end-sequent are interpreted as more or less expensive strategies for I to defend the corresponding claim. This leads to a new kind of labelled calculus, which can be seen as a fragment of SELL (subexponential linear logic). Finally, we generalize the concept of costs in proofs by using a semiring structure, illustrate our interpretation by examples and investigate some proof-theoretical properties.

The talk assumes no prior knowledge on games or substructural logic. Only a basic notion of sequent systems is advisable.

This is a joint work with Timo Lang, Carlos Olarte and Christian G. Fermüller.

Horário: 10:00 (UTC-3)

Prof. Lourdes González Huesca

National Autonomous University of Mexico (UNAM)

Abstract: In this talk, I will present the ongoing work to relate different deduction systems for constructive logic S4. Continuing our previous work, an equivalence between axiomatic and natural deduction, we study the equivalence between them with a dual-context sequent calculus. Sequent system GS4 uses sequents with two contexts to capture the notions of global and local truths without resorting to any formal semantics. Moreover, the dual-context approach allows us to manipulate modal formulas in the contexts by considering them as pure (non-modal) propositions and vice versa. This feature considerably simplifies the actual construction of proofs and sometimes allows us to replace modal reasoning with a simpler propositional one.

Joint work with Favio Miranda and Selene Linares.

Horário: 11:00 (UTC-3)

Claudia Orduz Siabato (mestranda)

Departamento de Matemática

Universidade de Brasília

Abstract. In this talk we present an extension of lambda calculus which models the consumption of resources, called the lambda calculus with resources . The idea of comparing languages such as pi- calculus, lambda calculus or lazy calculus led to the need to extend the syntax of these languages; hence the notion of multiplicity calculation and with it the calculation of resources. We will give an overview of the lambda calculus with resources: its syntax, reduction rules, examples and also illustrate the differences with the standard lambda calculus. Due to the non-deterministic characteristic of this new calculus, the notion of solvability extends to two notions different notions: may- and must- solvability. We will introduce both kinds of solvability and present some examples.

Time: 10:00 (UTC-3)

Andrés González (mestrando)

Departamento de Matemática

Universidade de Brasília

Abstract. One of the objectives when we are working with rewriting systems is to find convergent rewriting systems, that is, confluent and the terminating. These systems in rewriting theory are used to solve decision problems such as the word problem, which consists of deciding whether two expressions (or words) are equivalent from a set of identities E. There are several completion algorithms, within which the Knuth-Bendix algorithm [2], or also from Monoid algebra [3]. This talk will show the relationship of the linear operators, idempotent to represent concepts such as termination, confluence, and approaching completion from an algebraic point of view [1]

Time: 10:40 (UTC-3)

Prof. Delia Kesner

Université de Paris, CNRS, IRIF

Institut Universitaire de France

Abstract. 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.

Time: 10:00 (UTC-3)

Slides: https://drive.google.com/file/d/1O0ICSKrr3LTw6gsxE6QigY_2LwP30w4g/view?usp=sharing

Prof. Jorge A. Pérez (U. Groningen)

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.

Time: 10:30 (UTC-3)

Slides:https://drive.google.com/file/d/10F43vetnQEQpTEn8AwJDHy2L4PKdm2r8/view?usp=sharing

Prof. Carlos Olarte (ECT - UFRN)

Abstract: Linear logic (LL) has been used as a foundation (and inspiration) for the development of programming languages, logical frameworks and models for concurrency. In this talk, we shall see how to use the meta-theory of LL to (semi-automatically) prove the cut-elimination theorem for different object logics (OL) including propositional classical, minimal and intuitionistic logics. By considering a variant of LL with subexponentials, it is possible to extend these results to a wider range of logics including the modal logics K, 4, KT, KD and S4. Impressively enough, the sufficient conditions for cut-elimination of OLs are rather simple and easy to prove inside the LL framework. I will also present some technical details on how to formalize these results in the proof assistant Coq. All in all, we shall see how to encode and prove inside LL proof-theoretic properties of different logical systems that are widely used in philosophy, mathematics and computer science.

Time: 10:30 (UTC-3)

Slides: https://drive.google.com/file/d/11TmIJzgrue1Pc9wwBPKkHzZYN_Ey8sUZ/view?usp=sharing