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:20260422T225700Z
UID:LoReL/1
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LoReL/1/">Th
 e Machinery of Interaction</a>\nby Beniamino Accattoli (Inria\, France) as
  part of LoReL Seminar\n\n\nAbstract\nGirard's geometry of interaction sug
 gests an unusual way of evaluating lambda terms\, the interaction abstract
  machine (IAM)\, first studied by Mackie and Danos & Regnier in the nineti
 es\, using linear logic proof nets. In particular\, the IAM does not use e
 nvironments\, in contrast to the mainstream approach to abstract machines.
  In this talk I shall give a slow paced introduction to the IAM\, using an
  alternative presentation based on ordinary lambda terms. If time permits\
 , I shall also discuss how to measure the time and space consumptions of t
 he IAM via multi types. This talk is an overview of joint works with Ugo D
 al Lago and Gabriele Vanoni.\n
LOCATION:https://researchseminars.org/talk/LoReL/1/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alberto Pardo (Universidad de la República\, Uruguay)
DTSTART:20210429T170000Z
DTEND:20210429T180000Z
DTSTAMP:20260422T225700Z
UID:LoReL/2
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LoReL/2/">Fo
 rmalización de una transformación entre programas seguros usando un abor
 daje internalista</a>\nby Alberto Pardo (Universidad de la República\, Ur
 uguay) as part of LoReL Seminar\n\n\nAbstract\nLos lenguajes funcionales f
 uertemente tipados\, como Haskell\, OCaml\, Agda o Idris\, entre otros\, s
 e destacan por sus sistemas de tipos. Gracias a sus poderosos mecanismos d
 e tipado (llamense tipos dependientes\, GADTs\, funciones a nivel de tipos
 \, múltiples kinds\, type classes\, etc) uno puede ir más allá del uso 
 habitual que tienen los tipos en un lenguaje de programación y pasar a us
 arlos para para representar propiedades de los datos que manipula un progr
 ama (los llamados invariantes de tipos). Más allá del impacto (y dificul
 tad) que esto pueda implicar en la tarea de programación\, un benificio i
 mportante es que los invariantes pasan a formar parte del código ordinari
 o del programa y por lo tanto pueden ser verificados en tiempo de compilac
 ión por el chequeador de tipos del lenguaje. Es decir\, sólo son aceptad
 os aquellos programas que preservan los invariantes que tienen definidos e
 n sus tipos. Esta metodología de programación juega un rol clave\, por e
 jemplo\, en el desarrollo de software confiable. Al momento de codificar l
 os 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 predicad
 os 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 q
 ue uno codifica el invariante como parte de la propia definición del tipo
 . De esta forma\, se chequea la propiedad en la propia construcción de lo
 s términos del tipo y por lo tanto sólo es posible construir aquellos t
 érminos que satisfacen el invariante. En esta charla analizaremos un ejem
 plo en particular donde aplicamos esta metodología de programación con i
 nvariantes. 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 tom
 a programas seguros según un sistema flow-sensitive (en el que el nivel d
 e seguridad de las variables puede mudar) y los transforma en programas se
 guros tipables según un sistema flow-insensitive (en el que el nivel de s
 eguridad de las variables es fijo). Lo interesante de nuestra formalizaci
 ón es que está desarrollada usando el abordaje internalista.\n
LOCATION:https://researchseminars.org/talk/LoReL/2/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Octavio Malherbe (Universidad de la República\, Uruguay)
DTSTART:20210506T170000Z
DTEND:20210506T180000Z
DTSTAMP:20260422T225700Z
UID:LoReL/3
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LoReL/3/">Ca
 tegorías indexadas\, tripos y realizabilidad</a>\nby Octavio Malherbe (Un
 iversidad de la República\, Uruguay) as part of LoReL Seminar\n\n\nAbstra
 ct\nEn esta charla comenzaremos  con una introducción a las categorías i
 ndexadas para luego adentrarnos con un ejemplo de estas mediante la noció
 n de tripos. Esta herramienta nos permite modelar la lógica de alto orden
  y nos va  permitir  trabajar con ciertas abstracciones de la realizabilid
 ad clásica de Krivine  denominadas Abstract Krivine Structure (AKS) y cie
 rtas álgebras combinatorias (denominadas full adjunction ordered combinat
 ory algebras).  Veremos cómo de una AKS se determina una de estas álgebr
 as y en el otro sentido estas determinan un AKS para que sus tripos sean e
 quivalentes.\n
LOCATION:https://researchseminars.org/talk/LoReL/3/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrés Viso (Software Heritage\, France and UNQ\, Argentina)
DTSTART:20210527T170000Z
DTEND:20210527T180000Z
DTSTAMP:20260422T225700Z
UID:LoReL/4
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LoReL/4/">En
 coding Tight Typing in a Unified Framework</a>\nby Andrés Viso (Software 
 Heritage\, France and UNQ\, Argentina) as part of LoReL Seminar\n\n\nAbstr
 act\nThis joint work with Delia Kesner explores how the intersection type 
 theories of call-by-name (CBN) and call-by-value (CBV) can be unified in a
  more general framework provided by call-by-push-value (CBPV). Indeed\, we
  propose tight type systems for CBN and CBV that can be both encoded in a 
 tight type system for CBPV. All such systems are quantitative\, in the sen
 se that they provide exact information about the length of normalization s
 equences to normal form as well as the size of these normal forms. Moreove
 r\, the length of sequences to normal forms are discriminated according to
  their multiplicative/exponential nature\, a concept inherited from linear
  logic.\n
LOCATION:https://researchseminars.org/talk/LoReL/4/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Éric Tanter (Universidad de Chile\, Chile)
DTSTART:20210520T170000Z
DTEND:20210520T180000Z
DTSTAMP:20260422T225700Z
UID:LoReL/5
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LoReL/5/">Gr
 adualizing the Calculus of Inductive Constructions</a>\nby Éric Tanter (U
 niversidad de Chile\, Chile) as part of LoReL Seminar\n\n\nAbstract\n(join
 t work with M. Bertrand\, K. Maillard\, N. Tabareau)\n\nAcknowledging the 
 ordeal of a fully formal development in a proof assistant such as Coq\, we
  investigate gradual variations on the Calculus of Inductive Construction 
 (CIC) for swifter prototyping with imprecise types and terms. We observe\,
  with a no-go theorem\, a crucial tradeoff between graduality and the key 
 properties of canonicity\, decidability and closure of universes under dep
 endent product that CIC enjoys. Beyond this Fire Triangle of Graduality\, 
 we explore the gradualization of CIC with three different compromises\, ea
 ch relaxing one edge of the Fire Triangle. We develop a parametrized prese
 ntation of Gradual CIC that encompasses all three variations\, and jointly
  develop their metatheory. We first present a bidirectional elaboration of
  Gradual CIC to a dependently-typed cast calculus\, which elucidates the i
 nterrelation between typing\, conversion\, and graduality. We then establi
 sh the metatheory of this cast calculus through both a syntactic model int
 o CIC\, which provides weak canonicity\, confluence\, and when applicable\
 , normalization\, and a monotone model that purports the study of the grad
 uality of two of the three variants. This work informs and paves the way t
 owards the development of malleable proof assistants and dependently-typed
  programming languages.\n\n[The talk will be on the “intro material” o
 f the paper\, namely the analysis that leads to the Fire Triangle\, and no
 t on the gory technical details of the metatheory of Gradual CIC]\n
LOCATION:https://researchseminars.org/talk/LoReL/5/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Daniel Ventura (Universidade Federal de Goiás\, Brazil)
DTSTART:20210624T170000Z
DTEND:20210624T180000Z
DTSTAMP:20260422T225700Z
UID:LoReL/6
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LoReL/6/">Sk
 eletons Out! The Spirit of Node Replication</a>\nby Daniel Ventura (Univer
 sidade Federal de Goiás\, Brazil) as part of LoReL Seminar\n\n\nAbstract\
 n(joint work with Delia Kesner and Loïc Peyrot)\n\nIn this talk we introd
 uce a term calculus implementing higher-order node replication\, where sub
 stitution of terms are executed constructor by constructor. Besides implem
 enting the full node replication\, two evaluation strategies are considere
 d --call-by-name and fully lazy call-by-need-- based on the key notion of 
 skeleton\, with skeleton extraction internally codified in the calculus. O
 bservational equivalence between strategies is proved through a standard n
 on-idempotent intersection type system.\n
LOCATION:https://researchseminars.org/talk/LoReL/6/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Rafael Romero (Universidad de Buenos Aires\, Argentina)
DTSTART:20210701T170000Z
DTEND:20210701T180000Z
DTSTAMP:20260422T225700Z
UID:LoReL/7
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LoReL/7/">A 
 note on confluence in typed probabilistic lambda calculi</a>\nby Rafael Ro
 mero (Universidad de Buenos Aires\, Argentina) as part of LoReL Seminar\n\
 n\nAbstract\n(joint work with Alejandro Díaz-Caro)\n\nOn the topic of pro
 babilistic rewriting\, there are several works studying both termination a
 nd confluence of different systems. While working with a lambda calculus m
 odelling quantum computation\, we found a system with probabilistic rewrit
 ing rules and strongly normalizing terms. We examine the effect of small m
 odifications in probabilistic rewriting\, affine variables\, and strategie
 s on the overall confluence in this strongly normalizing probabilistic cal
 culus.\n
LOCATION:https://researchseminars.org/talk/LoReL/7/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Malena Ivnisky (Universidad de Buenos Aires\, Argentina)
DTSTART:20210708T170000Z
DTEND:20210708T180000Z
DTSTAMP:20260422T225700Z
UID:LoReL/8
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LoReL/8/">A 
 finite-dimensional model for affine\, linear quantum lambda calculi with g
 eneral recursion</a>\nby Malena Ivnisky (Universidad de Buenos Aires\, Arg
 entina) as part of LoReL Seminar\n\n\nAbstract\n(joint work with Alejandro
  Díaz-Caro\, Hernán Melgratti\, and Benoît Valiron)\n\nWe introduce a c
 oncrete domain model for the quantum lambda calculus and lambda-rho extend
 ed with a fixpoint operator. A distinctive feature of lambda-rho is that i
 t relies on density matrices for describing both quantum information and p
 robabilistic distributions over computation states. It has been shown that
  there is a conservative translation from lambda-rho to the quantum lambda
  calculus of Selinger and Valiron. In contrast to existing models for quan
 tum lambda calculi featuring recursion with intuitionistic arrows\, our mo
 del is finite-dimensional and does not need more than cones of positive ma
 trices and affine arrows.\n
LOCATION:https://researchseminars.org/talk/LoReL/8/
END:VEVENT
END:VCALENDAR