BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Beniamino Accattoli (Inria\, France) DTSTART:20210422T170000Z DTEND:20210422T180000Z DTSTAMP:20260404T131154Z UID:LoReL/1 DESCRIPTION:Title: The Machinery of Interaction\nby Beniamino Accattoli (Inria\, Fra nce) as part of LoReL Seminar\n\n\nAbstract\nGirard's geometry of interact ion suggests an unusual way of evaluating lambda terms\, the interaction a bstract machine (IAM)\, first studied by Mackie and Danos & Regnier in the nineties\, using linear logic proof nets. In particular\, the IAM does no t use environments\, in contrast to the mainstream approach to abstract ma chines. In this talk I shall give a slow paced introduction to the IAM\, u sing an alternative presentation based on ordinary lambda terms. If time p ermits\, I shall also discuss how to measure the time and space consumptio ns of the IAM via multi types. This talk is an overview of joint works wit h Ugo Dal Lago and Gabriele Vanoni.\n LOCATION:https://stable.researchseminars.org/talk/LoReL/1/ END:VEVENT BEGIN:VEVENT SUMMARY:Alberto Pardo (Universidad de la República\, Uruguay) DTSTART:20210429T170000Z DTEND:20210429T180000Z DTSTAMP:20260404T131154Z UID:LoReL/2 DESCRIPTION:Title: Formalización de una transformación entre programas seguros usando un abordaje internalista\nby Alberto Pardo (Universidad de la Repúbli ca\, Uruguay) as part of LoReL Seminar\n\n\nAbstract\nLos lenguajes funcio nales fuertemente tipados\, como Haskell\, OCaml\, Agda o Idris\, entre ot ros\, se destacan por sus sistemas de tipos. Gracias a sus poderosos mecan ismos de tipado (llamense tipos dependientes\, GADTs\, funciones a nivel d e tipos\, múltiples kinds\, type classes\, etc) uno puede ir más allá d el uso habitual que tienen los tipos en un lenguaje de programación y pas ar a usarlos para para representar propiedades de los datos que manipula u n programa (los llamados invariantes de tipos). Más allá del impacto (y dificultad) que esto pueda implicar en la tarea de programación\, un beni ficio importante es que los invariantes pasan a formar parte del código o rdinario del programa y por lo tanto pueden ser verificados en tiempo de c ompilación por el chequeador de tipos del lenguaje. Es decir\, sólo son aceptados aquellos programas que preservan los invariantes que tienen defi nidos en sus tipos. Esta metodología de programación juega un rol clave\ , por ejemplo\, en el desarrollo de software confiable. Al momento de codi ficar los invariantes a nivel de los tipos existen distintas alternativas. Una es la estándar\, en la que uno asocia los invariantes a través de p redicados por fuera de la definición de los tipos. A este abordaje se le llama "externalista". Otra opción es usando un abordaje "internalista"\, en el que uno codifica el invariante como parte de la propia definición d el tipo. De esta forma\, se chequea la propiedad en la propia construcció n de los términos del tipo y por lo tanto sólo es posible construir aque llos términos que satisfacen el invariante. En esta charla analizaremos u n ejemplo en particular donde aplicamos esta metodología de programación con invariantes. En concreto\, vamos a mostrar la formalización en Agda de una transformación entre programas seguros (de un lenguaje imperativo simple) que preserva la propiedad de no interferencia. Dicha transformaci ón toma programas seguros según un sistema flow-sensitive (en el que el nivel de seguridad de las variables puede mudar) y los transforma en progr amas seguros tipables según un sistema flow-insensitive (en el que el niv el de seguridad de las variables es fijo). Lo interesante de nuestra forma lización es que está desarrollada usando el abordaje internalista.\n LOCATION:https://stable.researchseminars.org/talk/LoReL/2/ END:VEVENT BEGIN:VEVENT SUMMARY:Octavio Malherbe (Universidad de la República\, Uruguay) DTSTART:20210506T170000Z DTEND:20210506T180000Z DTSTAMP:20260404T131154Z UID:LoReL/3 DESCRIPTION:Title: Categorías indexadas\, tripos y realizabilidad\nby Octavio Malhe rbe (Universidad de la República\, Uruguay) as part of LoReL Seminar\n\n\ nAbstract\nEn esta charla comenzaremos con una introducción a las catego rías indexadas para luego adentrarnos con un ejemplo de estas mediante la noción de tripos. Esta herramienta nos permite modelar la lógica de alt o orden y nos va permitir trabajar con ciertas abstracciones de la reali zabilidad clásica de Krivine denominadas Abstract Krivine Structure (AKS ) y ciertas álgebras combinatorias (denominadas full adjunction ordered c ombinatory algebras). Veremos cómo de una AKS se determina una de estas álgebras y en el otro sentido estas determinan un AKS para que sus tripos sean equivalentes.\n LOCATION:https://stable.researchseminars.org/talk/LoReL/3/ END:VEVENT BEGIN:VEVENT SUMMARY:Andrés Viso (Software Heritage\, France and UNQ\, Argentina) DTSTART:20210527T170000Z DTEND:20210527T180000Z DTSTAMP:20260404T131154Z UID:LoReL/4 DESCRIPTION:Title: Encoding Tight Typing in a Unified Framework\nby Andrés Viso (So ftware Heritage\, France and UNQ\, Argentina) as part of LoReL Seminar\n\n \nAbstract\nThis joint work with Delia Kesner explores how the intersectio n type theories of call-by-name (CBN) and call-by-value (CBV) can be unifi ed in a more general framework provided by call-by-push-value (CBPV). Inde ed\, we propose tight type systems for CBN and CBV that can be both encode d in a tight type system for CBPV. All such systems are quantitative\, in the sense that they provide exact information about the length of normaliz ation sequences to normal form as well as the size of these normal forms. Moreover\, the length of sequences to normal forms are discriminated accor ding to their multiplicative/exponential nature\, a concept inherited from linear logic.\n LOCATION:https://stable.researchseminars.org/talk/LoReL/4/ END:VEVENT BEGIN:VEVENT SUMMARY:Éric Tanter (Universidad de Chile\, Chile) DTSTART:20210520T170000Z DTEND:20210520T180000Z DTSTAMP:20260404T131154Z UID:LoReL/5 DESCRIPTION:Title: Gradualizing the Calculus of Inductive Constructions\nby Éric Ta nter (Universidad de Chile\, Chile) as part of LoReL Seminar\n\n\nAbstract \n(joint work with M. Bertrand\, K. Maillard\, N. Tabareau)\n\nAcknowledgi ng the ordeal of a fully formal development in a proof assistant such as C oq\, we investigate gradual variations on the Calculus of Inductive Constr uction (CIC) for swifter prototyping with imprecise types and terms. We ob serve\, with a no-go theorem\, a crucial tradeoff between graduality and t he key properties of canonicity\, decidability and closure of universes un der dependent product that CIC enjoys. Beyond this Fire Triangle of Gradua lity\, we explore the gradualization of CIC with three different compromis es\, each relaxing one edge of the Fire Triangle. We develop a parametrize d presentation of Gradual CIC that encompasses all three variations\, and jointly develop their metatheory. We first present a bidirectional elabora tion of Gradual CIC to a dependently-typed cast calculus\, which elucidate s the interrelation between typing\, conversion\, and graduality. We then establish the metatheory of this cast calculus through both a syntactic mo del into CIC\, which provides weak canonicity\, confluence\, and when appl icable\, normalization\, and a monotone model that purports the study of t he graduality of two of the three variants. This work informs and paves th e way towards the development of malleable proof assistants and dependentl y-typed programming languages.\n\n[The talk will be on the “intro materi al” of the paper\, namely the analysis that leads to the Fire Triangle\, and not on the gory technical details of the metatheory of Gradual CIC]\n LOCATION:https://stable.researchseminars.org/talk/LoReL/5/ END:VEVENT BEGIN:VEVENT SUMMARY:Daniel Ventura (Universidade Federal de Goiás\, Brazil) DTSTART:20210624T170000Z DTEND:20210624T180000Z DTSTAMP:20260404T131154Z UID:LoReL/6 DESCRIPTION:Title: Skeletons Out! The Spirit of Node Replication\nby Daniel Ventura (Universidade Federal de Goiás\, Brazil) as part of LoReL Seminar\n\n\nAb stract\n(joint work with Delia Kesner and Loïc Peyrot)\n\nIn this talk we introduce a term calculus implementing higher-order node replication\, wh ere substitution of terms are executed constructor by constructor. Besides implementing the full node replication\, two evaluation strategies are co nsidered --call-by-name and fully lazy call-by-need-- based on the key not ion of skeleton\, with skeleton extraction internally codified in the calc ulus. Observational equivalence between strategies is proved through a sta ndard non-idempotent intersection type system.\n LOCATION:https://stable.researchseminars.org/talk/LoReL/6/ END:VEVENT BEGIN:VEVENT SUMMARY:Rafael Romero (Universidad de Buenos Aires\, Argentina) DTSTART:20210701T170000Z DTEND:20210701T180000Z DTSTAMP:20260404T131154Z UID:LoReL/7 DESCRIPTION:Title: A note on confluence in typed probabilistic lambda calculi\nby Ra fael Romero (Universidad de Buenos Aires\, Argentina) as part of LoReL Sem inar\n\n\nAbstract\n(joint work with Alejandro Díaz-Caro)\n\nOn the topic of probabilistic rewriting\, there are several works studying both termin ation and confluence of different systems. While working with a lambda cal culus modelling quantum computation\, we found a system with probabilistic rewriting rules and strongly normalizing terms. We examine the effect of small modifications in probabilistic rewriting\, affine variables\, and st rategies on the overall confluence in this strongly normalizing probabilis tic calculus.\n LOCATION:https://stable.researchseminars.org/talk/LoReL/7/ END:VEVENT BEGIN:VEVENT SUMMARY:Malena Ivnisky (Universidad de Buenos Aires\, Argentina) DTSTART:20210708T170000Z DTEND:20210708T180000Z DTSTAMP:20260404T131154Z UID:LoReL/8 DESCRIPTION:Title: A finite-dimensional model for affine\, linear quantum lambda calculi with general recursion\nby Malena Ivnisky (Universidad de Buenos Aire s\, Argentina) as part of LoReL Seminar\n\n\nAbstract\n(joint work with Al ejandro Díaz-Caro\, Hernán Melgratti\, and Benoît Valiron)\n\nWe introd uce a concrete domain model for the quantum lambda calculus and lambda-rho extended with a fixpoint operator. A distinctive feature of lambda-rho is that it relies on density matrices for describing both quantum informatio n and probabilistic distributions over computation states. It has been sho wn that there is a conservative translation from lambda-rho to the quantum lambda calculus of Selinger and Valiron. In contrast to existing models f or quantum lambda calculi featuring recursion with intuitionistic arrows\, our model is finite-dimensional and does not need more than cones of posi tive matrices and affine arrows.\n LOCATION:https://stable.researchseminars.org/talk/LoReL/8/ END:VEVENT END:VCALENDAR