LoReL: Logic and Rewriting for Programming Languages, is a research team at UNQ and ICC (UBA/CONICET). The topics of interest include: Rewriting and Lambda Calculus, Type Theory, and Logical Methods with a focus on their application to Programming Languages, both, for classical and quantum computing.

Latest publications

• A. Díaz-Caro and M. Villagra. Classically time-controlled quantum automata: Definition and properties
  The Computer Journal, to appear, 2024.
• A. Díaz-Caro. Lógica y computación cuántica: Un camino a través de los vaivenes políticos de la Argentina
  In Bits de Ciencia, 26:20-25, 2024.
• A. Díaz-Caro, G. Dowek, M. Ivnisky, and O. Malherbe. A linear proof language for second-order intuitionistic linear logic
  In Proceedings of WoLLIC 2024, at LNCS 14672:18-35, 2024.
• A. Díaz-Caro and G. Dowek. A linear linear lambda-calculus
  Mathematical Structures in Computer Science, First View, pages 1-35, 2024.
• B. Accattoli and P. Barenbaum. A Diamond Machine for Strong Evaluation
  In Proceedings of APLAS 2023, at LNCS 14405:69-90, 2023.

• A. Díaz-Caro and O. Malherbe. A concrete model for a typed linear algebraic lambda calculus
  Mathematical Structures in Computer Science, 34(1):1-40, 2023.
• A. Díaz-Caro and G. Dowek. Extensional proofs in a propositional logic modulo isomorphisms
  Theoretical Computer Science, 977:114172, 2023.
• R. Kuhn, H. C. Melgratti, and E. Tuosto. Behavioural Types for Local-First Software
  In Proceedings of ECOOP 2023, at LIPIcs 263:15, 2023.
• H. C. Melgratti, C. A. Mezzina, and G. M. Pinna. Relating Reversible Petri Nets and Reversible Event Structures, Categorically
  In Proceedings of FORTE 2023, at LNCS 13910:206-223, 2023.
• P. Barenbaum and C. Sottile. Two Decreasing Measures for Simply Typed Lambda-Terms
  In Proceedings of FSCD 2023, at LIPIcs 260:11, 2023.
• A. Díaz-Caro and G. Dowek. A New Connective in Natural Deduction, and its Application to Quantum Computing
  Theoretical Computer Science, 957:113840, 2023.
• R. De Nicola and H. C. Melgratti. Multiparty testing preorders
  Logical Methods in Computer Science, 19(1:1), 2023.
• P. Barenbaum and T. Freund. Proofs and Refutations for Intuitionistic and Second-Order Logic
  In Proceedings of CSL 2023, at LIPIcs 252:9, 2023.
• P. Barenbaum and E. Bonelli. Reductions in Higher-Order Rewriting and Their Equivalence
  In Proceedings of CSL 2023, at LIPIcs 252:8, 2023.
• A. Díaz-Caro and O. Malherbe. Quantum control in the unitary sphere: Lambda-S₁ and its categorical model
  Logical Methods in Computer Science, 18(3:32), 2022.
• A. Borgna and R. Romero. Encoding High-level Quantum Programs as SZX-diagrams
  In Proceedings of QPL 2022, volume 394 of Electronic Proceedings in Theoretical Computer Science, pages 141-169, 2022.
• U. de'Liguoro, H. C. Melgratti, and E. Tuosto. Towards refinable choreographies
  Journal of Logical and Algebraic Methods in programming, 127:100776, 2022.
• A. Díaz-Caro and G. Dowek. Linear lambda calculus is linear
  In Proceedings of FSCD 2022, at LIPIcs 228:21, 2022.
• H. C. Melgratti, C. Antares Mezzina, and G. M. Pinna. A Petri net view of covalent bonds
  Theoretical Computer Science 908:89-119, 2022.
• F. Gadducci, H. C. Melgratti, C. Roldán, and M. Sammartino. Categorical specification and implementation of Replicated Data Types
  Theoretical Computer Science 903:84-112, 2022.
• R. Romero and A. Díaz-Caro. A note on confluence in typed probabilistic lambda calculi
  In Proceedings of LSFA 2021, volume 357 of Electronic Proceedings in Theoretical Computer Science pages 18-24, 2021.
• A. Díaz-Caro. A quick overview on the quantum control approach to the lambda calculus
  In Proceedings of LSFA 2021 (invited paper), volume 357 of Electronic Proceedings in Theoretical Computer Science pages 1-17, 2021.
• D. Kesner and A. Viso. Encoding Tight Typing in a Unified Framework
  In Procedings of CSL 2022, volume 216 of Leibniz International Proceedings in Informatics (LIPIcs), article 27, 2021.
• A. Díaz-Caro and G. Dowek. A New Connective in Natural Deduction, and its Application to Quantum Computing
  In Procedings of ICTAC 2021, volume 12819 of Lecture Notes in Computer Science, pages 175-193, 2021.
• H. C. Melgratti, C. Antares Mezzina, and G. Michele Pinna. A distributed operational view of Reversible Prime Event Structures
  In Procedings of LICS 2021, 2021.
• P. Barenbaum and T. Freund. A Constructive Logic with Classical Proofs and Refutations
  In Procedings of LICS 2021, 2021.
• H. C. Melgratti, C. Antares Mezzina, and G. Michele Pinna. Towards a Truly Concurrent Semantics for Reversible CSS
  In ACM Procedings of RC 2021, volume 12805 of Lecture Notes in Computer Science, pages 109-125, 2021.
• C. F. Sottile, A. Díaz-Caro, and P. E. Martínez López. Polymorphic System I
  In ACM Procedings of IFL 2020, pages 127-137, 2020.
• P. Barenbaum, F. Lochbaum, and M. Milicich. Semantics of a Relational λ-Calculus
  In Proceedings of ICTAC 2020, volume 12545 of Lecture Notes in Computer Science, pages 242-261, 2020.
• P. Barenbaum and E. Bonelli. Rewrites as Terms through Justification Logic
  In Proceedings of PPDP 2020, article 12, ACM, 2020.
• A. Martín, A. Ríos, and A. Viso. Pure Pattern Calculus a la de Bruijn
  In Proceedings of LSFA 2020, volume 351 of Electronic Notes in Theoretical Computer Science, pages 95-113, 2020.
• A. Díaz-Caro and O. Malherbe. A Categorical Construction for the Computational Definition of Vector Spaces
  Applied Categorical Structures 28(5):807-844, 2020.
• A. Bucciarelli, D. Kesner, A. Ríos, and A. Viso. The Bang Calculus Revisited
  In Proceedings of FLOPS 2020, volume 12073 of Lecture Notes in Computer Science, pages 13-32, 2020.
• B. Accattoli and A. Díaz-Caro. Functional Pearl: The Distributive λ-Calculus
  In Proceedings of FLOPS 2020, volume 12073 of Lecture Notes in Computer Science, pages 33-49, 2020.
• D. Kesner, E. Bonelli, and A. Viso. Strong Bisimulation for Control Operators (invited talk)
  In Proceedings of CSL 2020, volume 152 of Leibniz International Proceedings in Informatics (LIPIcs), article 4, 2020.
• F. Olmedo and A. Díaz-Caro. Runtime Analysis of Quantum Programs: A Formal Approach
  Extended abstract at PLanQC. 2020.
• A. Díaz-Caro, G. Dowek, and J. P. Rinaldi. Two linearities for quantum computing in the lambda calculus
  Postproceedings of TPNC'2017 at BioSystems 186:104012, 2019.
• M. Ayala-Rincón, E. Bonelli, J. Edi, and A. Viso. Typed path polymorphism
  Theoretical Computer Science 781:111-130, 2019.
• A. Díaz-Caro and O. Malherbe. A categorical construction for the computational definition of vector spaces (extended abstract)
  Extended abstract at ACT 2019. 2019.
• A. Díaz-Caro and G. Dowek. Proof Normalisation in a Logic Identifying Isomorphic Propositions
  In H. Geuvers, editor, Proceedings of FSCD 2019, volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), article 14, 2019.
• A. Díaz-Caro, M. Guillermo, A. Miquel, and B. Valiron. Realizability in the Unitary Sphere
  In Proceedings of LICS 2019, 2019.
• P. Barenbaum and G. Ciruelos. Factoring Derivation Spaces via Intersection Types
  In S. Ryu, editor, Proceedings of APLAS 2018, volume 11275 of Lecture Notes in Computer Science, pages 22-44, 2018.
• A. Díaz-Caro and M. Villagra. Classically time-controlled quantum automata
  In C. Martín-Vide, M. O'Neill, and M.A. Vega-Rodríguez, editors, Proceedings of TPNC 2018, volume 11324 of Lecture Notes in Computer Science, pages 266-278, 2018.
• A. Díaz-Caro and O. Malherbe. A concrete categorical semantics for Lambda-S
  In Proceedings of LSFA 2018, volume 344 of Electronic Notes in Theoretical Computer Science, pages 83-100, 2019.
• P. Barenbaum, E. Bonelli, and K. Mohamed. Pattern Matching and Fixed Points: Resource Types and Strong Call-By-Need.
  In D. Sabel, editor, Proceedings of PPDP 2018, ACM, Article 6, 2018.
• D. Kesner, A. Ríos, and A. Viso. Call-by-need, neededness and all that.
  In C. Baier and U. Dal Lago, editors, Proceedings of FoSSaCS 2018, volume 10803 of Lecture Notes in Computer Science, pages 241-257, 2018.
• J. Edi, A. Viso, and E. Bonelli. Efficient type checking for path polymorphism.
  In T. Uustalu, editor, Postproceedings of TYPES 2015, volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:23, 2018.
• A. Díaz-Caro and G. Dowek. Typing quantum superpositions and measurement.
  In C. Martín-Vide, R. Neruda, and M. A. Vega-Rodríguez, editors, Proceedings of TPNC 2017, volume 10687 of Lecture Notes in Computer Science, pages 281-293, 2017.
• A. Díaz-Caro. A lambda calculus for density matrices with classical and probabilistic controls.
  In B.-Y. E. Chang, editor, Proceedings of APLAS 2017, volume 10695 of Lecture Notes in Computer Science, pages 448-467, 2017.
• A. Díaz-Caro and G. Martínez. Confluence in probabilistic rewriting.
  In S. Alves and R. Wassermann, editors, Preproceedings of LSFA 2017, volume 338 of Electronic Notes in Theoretical Computer Science, pages 115-131, 2018.
• P. Arrighi, A. Díaz-Caro, and B. Valiron. The vectorial lambda-calculus.
  Information and Computation, 254(1):105-139, 2017.
• E. Bonelli, D. Kesner, C. Lombardi, and A. Ríos. On abstract normalisation beyond neededness.
  Theoretical Computer Science, 672:36-63, 2017.
• M. Coppo, M. Dezani-Ciancaglini, A. Díaz-Caro, I. Margaria, and M. Zacchi. Retractions in intersection types.
  In N. Kobayashi, editor, Proceedings of ITRS 2016, volume 242 of Electronic Proceedings in Theoretical Computer Science, pages 31-47, 2017.
• A. Viso, E. Bonelli, and M. Ayala-Rincón. Type soundness for path polymorphism.
  In M. Benevides and R. Thiemann, editors, Proceedings LSFA 2015, volume 323 of Electronic Notes in Theoretical Computer Science, pages 235-251, 2016.
• A. Díaz-Caro and A. Yakaryılmaz. Affine computation and affine automaton.
  In A. Kulikov and G. Woeginger, editors, Proceedings of CSR 2016, volume 9691 of Lecture Notes in Computer Science, pages 146-160, 2016.
• A. Díaz-Caro and P. E. Martínez López. Isomorphisms considered as equalities: Projecting functions and enhancing partial application through an implementation of λ⁺.
  In R. Lammel, editor, Proceedings of IFL 2015, ACM, pages 9:1-9:11, 2015.
• F. Bavera and E. Bonelli. Justification logic and audited computation.
  Journal of Logic and Computation, exv037, 2015.
• B. Accattoli, P. Barenbaum, and D. Mazza. A strong distillery.
  In X. Feng and S. Park, editors, Proceedings of APLAS 2015, volume 9458 of Lecture Notes in Computer Science, pages 231-250, 2015.
• A. Assaf, A. Díaz-Caro, S. Perdrix, C. Tasson, and B. Valiron. Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus.
  Logical Methods in Computer Science, 10(4:8), 2014.
• B. Accattoli, P. Barenbaum, and D. Mazza. Distilling abstract machines.
  In M. W. Bailey, R. Balasubramonian, A. Davis, and S. Adve, editors, Proceedings of ICFP 2014, volume 49(9) of ACM SIGPLAN Notices, pages 363-376, 2014.
• C. Lombardi, A. Ríos, and R. de Vrijer. Proof terms for infinitary rewriting.
  In G. Dowek, editor, Proceedings of RTA 2014, volume 8560 of Lecture Notes in Computer Science, pages 303-318, 2014.
• E. Bonelli and G. Steren. Hypothetical logic of proofs.
  Logica Universalis, 8(1):103-140, 2014.
• B. Accattoli, E. Bonelli, D. Kesner, and C. Lombardi. A nonstandard standardization theorem.
  In M. W. Bailey, editor, Proceedings of POPL 2014, volume 49(1) of ACM SIGPLAN Notices, pages 659-670, 2014.
• G. Steren and E. Bonelli. Intuitionistic hypothetical logic of proofs.
  In V. de Paiva, M. Benevides, V. Nigam, and E. Pimentel, editors, Proceedings of IMLA 2013, volume 300 of Electronic Notes in Theoretical Computer Science, pages 89-103, 2014.
• E. Bonelli, D. Kesner, C. Lombardi, and A. Rios. Normalisation for dynamic pattern calculi.
  In A. Tiwari, editor, Proceedings of RTA 2012, volume 15 of Leibniz International Proceedings in Informatics (LIPIcs), pages 117-132, 2012.
• E. Bonelli and F. Feller. Justification logic as a foundation for certifying mobile computation.
  Annals of Pure and Applied Logic, 163(7):935-950, 2012.
• D. Kesner, C. Lombardi, and A. Ríos. A standardisation proof for algebraic pattern calculi.
  In E. Bonelli, editor, Proceedings HOR 2010, volume 49 of Electronic Proceedings in Theoretical Computer Science, pages 58-72, 2011.
• A. Mendelzon, A. Ríos, and B. Ziliani. Swapping: a natural bridge between named and indexed explicit substitution calculi.
  In E. Bonelli, editor, Proceedings HOR 2010, volume 49 of Electronic Proceedings in Theoretical Computer Science, pages 1-15, 2011.
• A. Arbiser, A. Miquel, and A. Ríos. The λ-calculus with constructors: Syntax, confluence and separation.
  Journal of Functional Programming, 19(5):581-631, 2009.

Upcoming seminar talks

• No upcoming seminar planned.

Past talks

• December 4, 2023 Giulio Guerrieri (Aix-Marseille Université): The theory of meaningfulness in the call-by-value lambda-calculus (hide)
  

  The untyped lambda-calculus is a simple and Turing-complete model of computation that represents the kernel of any functional programming language. The semantics of the untyped call-by-name lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different ways. In particular, unsolvable terms provide a consistent notion of meaningless terms, and meaningful terms can be identified with the solvable ones. The semantics of the untyped call-by-value lambda-calculus (CbV, which is closer to the real implementations of programming languages) is instead still in its infancy, because of some inherent difficulties but also because CbV solvable terms are less studied and understood than in call-by-name. On the one hand, we show that a carefully crafted presentation of CbV allows us to recover many of the properties that solvability has in call-by-name, in particular qualitative and quantitative characterizations via multi types. On the other hand, we stress that, in CbV, solvability plays a different role: identifying unsolvable terms as meaningless induces an inconsistent theory. We argue that in CbV, the correct notion of meaningful terms is captured by the concept of potential valuability. In particular, terms that are not potentially valuable provide a consistent notion of meaningless terms in CbV.

  15hs, sala 1604, Pabellón Cero + Infinito.
• November 7, 2023 Pablo Arrighi and Alejandro Díaz-Caro. Moderator: Ignacio Uman: Café de las Ciencias: computadora cuántica, ¿la computadora definitiva?
• November 8, 2023 Pablo Arrighi (LMF, Université Paris-Saclay): ¿Cuál es la diferencia entre el pasado y el futuro? (o "un modelo de juguete con flecha del tiempo demostrable sin hipótesis de pasado"). (hide)
  

  Las leyes de la Física son reversibles en el tiempo: no distinguen, cualitativamente hablando, el pasado del futuro. Sin embargo, sólo podemos ir hacia el futuro. Esta aparente contradicción se conoce como el "problema de la flecha del tiempo". Su resolución actual afirma que el futuro es la dirección del aumento de la entropía. Pero la entropía sólo puede aumentar hacia el futuro si ha sido baja en el pasado, y la baja entropía en el pasado es una suposición muy fuerte, porque los estados de baja entropía son totalmente improbables, no genéricos. No obstante, trabajos recientes de la literatura de Física sugieren que podemos deshacernos de dicha "hipótesis del pasado", en presencia de leyes dinámicas reversibles que presenten expansión. Demostramos que éste es el caso, para un modelo de juguete basado en la reescritura sincrónica de grafos. Consiste en grafos en los que las partículas circulan e interactúan según reglas locales reversibles. Algunas reglas achican o expanden localmente el grafo. Los estados genéricos siempre se expanden; la entropía siempre aumenta, ofreciendo así una explicación local de la flecha del tiempo. Este marco discreto permite desplegar todo el rigor de las técnicas de prueba de las ciencias de la computación.

  11hs, sala 1403, Pabellón Cero + Infinito.
• August 11, 2023 Mariana Milicich (Universidad de Paris Cité): Tipos cuantitativos para reducción útil
  
  (hide)
  Título: Tipos cuantitativos para reducción útil Resumen: El cálculo-λ permite expresar todas las funciones computables, pero, ¿puede ser una máquina "razonable" de acuerdo con la Tesis de la Invariancia de van Emde Boas? Definiendo la estrategia de evaluación "útil", Accattoli y Dal Lago pudieron responder afirmativamente a esta pregunta. Sin embargo, su caracterización no facilita el uso de argumentos inductivos para razonar sobre ella. Y, al día de la fecha, no existen modelos cuantitativos o herramientas para medir su complejidad temporal. Por eso, en esta charla voy a hablar de la primera caracterización inductiva de la evaluación "útil" para call-by-value abierto. Esto lo logramos parametrizando la relación de evaluación con respecto a la información que nos proporciona el contexto en el que está computando. Además, establecimos una relación entre esta evaluación y otra que también damos para call-by-value abierto, pero que no es "útil". Probamos que ambas estrategias conducen a las mismas formas normales módulo cierta operación. Lo último que voy a contar es que dimos un modelo para la estrategia útil usando un sistema de tipos intersección. Específicamente, trabajamos con tipos intersección no idempotentes y reglas ajustadas (o tight). Esto deviene en que nuestro modelo es cuantitativo: tipar un término t nos dice exactamente cuántos pasos requiere el cómputo para llevar t a forma normal.
  
  
• June 16, 2023 Edwin Pin (Universidad de Buenos Aires, Argentina): Camino a CPDL+
  
  (hide)
  Resumen: CPDL+ es un lenguaje que extiende al tradicional PDL con un operador nuevo que identifica patrones topológicos sobre estructuras con forma de grafos con datos. La intención original de este trabajo era caracterizar mediante un juego de bisimulación al conjunto de fórmulas ICPDL (PDL extendido con inversa y reverso), pero en el desarrollo de tal técnica obtuvimos resultados que introducen toda una familia de nuevos lenguajes y que generalizan otras lógicas como RPQ, Regular Queries o el ya mencionado ICPDL.
  
  
• June 2, 2023 Malena Ivnisky (Universidad de Buenos Aires, Argentina and Universidad de la República, Uruguay): Polimorfismo en el cálculo LS
  
  (hide)
  En este trabajo en progreso se presenta una extensión al cálculo LS, el lenguaje de pruebas de la lógica lineal aditiva-multiplicativa intuicionista con reglas intersticiales, diseñado para representar vectores y operadores en la computación cuántica. Esta extensión agrega polimorfismo y el operador !. El objetivo de este trabajo es definir una representación de vectores y operadores lineales que permita expresar algoritmos cuánticos polimórficos.
  
  
• May 5, 2023 Santiago Cifuentes (Universidad de Buenos Aires, Argentina): Data-graph repairing
  
  (hide)
  Las bases de datos con forma de grafo resultan ser un modelo de representación del conocimiento más conveniente que el relacional es un gran conjunto de aplicaciones modernas: el análisis de las redes sociales, de la Web Semántica o de la procedencia de los datos, entre otras. Para acceder a la información dentro del grafo se usan lenguajes navigacionales capaces de capturar propiedades interesantes, como expresiones regulares o graph patterns. Como en el caso relacional, al ser la información de la base de datos la representación de un área de interés, es natural que preserve carecterísticas heredadas del mundo que captura. Estas restricciones de integridad pueden ser incorporadas al modelo mediante alguno de los lenguajes ya nombrados, de la misma forma que las foreign keys del modelo relacional limitan la forma de los datos almacenados. Luego, el motor de base de datos es capaz de asegurar la satisfacción de estas reglas a través de las transacciones, bloqueando las mismas cuando rompen la "consistencia" de la información. No obstante, en distintas aplicaciones modernas es inevitable que las bases de datos muten de forma brusca, y que por lo tanto garantizar la consistencia en todo momento se vuelva costoso. Por lo tanto, se han desarrollado modelos tolerantas a la incosistencia, que permiten, dado un estado inconsistente, recuperar de alguna forma un subconjunto de los datos con alguna garantía de que sean correctos. En este contexto se plantea la noción de repair: dada una base de datos D, un repair de D es una nueva base de datos D' que difiera mínimamente de D y que sea consistente respecto a un conjunto de restricciones de integridad. Dependiendo de la definición de "diferir mínimamente" es posible que haya más de un repair, en cuyo caso es posible definir la noción de "consistent query answering" como aquel conjunto de respuestas que cualquier repair daría. Vamos a extender estas nociones a modelos de bases de datos con forma de grafo. En particular, estudiamos el problema de calcular algún repair dado un grafo G, e incluso el de calcular un repair preferido, dado un orden de preferencias sobre los grafos.
  
  
• April 21, 2023 Pablo Barenbaum (Universidad de Buenos Aires, Argentina and UNQ/CONICET, Argentina): Proof Terms for Higher-Order Rewriting and Their Equivalence
  
  (hide)
  Los proof terms son expresiones que representan cómputos en el marco de sistemas de reescritura de términos. Fueron propuestos por Meseguer y utilizados por van Oostrom y de Vrijer para estudiar la equivalencia de reducciones en sistemas de reescritura de primer orden. En este trabajo, en colaboración con Eduardo Bonelli, estudiamos el problema de extender la noción de proof term a sistemas de reescritura de orden superior, incluyendo la presencia de ligadores y sustitución. En trabajos precedentes, como el de Bruggink, se ha observado que el desafío consiste en reconciliar la composición de proof terms con la operación de sustitución (beta-equivalencia). Esto condujo a Bruggink a rechazar la presencia del operador de composición "anidado" dentro de otros constructores de términos. En este trabajo proponemos una noción de proof term que admite la presencia de composición anidada. Definimos dos nociones de equivalencia entre proof terms: equivalencia por permutación y equivalencia por proyección, y probamos que son equivalentes.
  
  
• December 5, 2022 Delia Kesner (Université Paris-Cité & Institut Universitaire de France): Embedding Quantitative Properties of Call-by-Name and Call-by-Value into Call-by-Push-Value .
  
  (hide)
  This talks explores how the (untyped and typed) 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 first present an untyped CBPV-like calculus, called lambda-bang, which encodes untyped CNB and CBV, both from a static and a dynamic point of view. We then explore these encodings in a typed framework, specified by quantitative (aka non-idempotent intersection) types. Three different (quantitative) properties are discussed. The first one is related to upper bounds for reduction lengths, the second one concerns exact measures for reduction lengths and sizes of normal forms, and the last one is about the inhabitation problem. In all these cases, explained and discussed in the talk, the (quantitative) property for CBN/CBV is inherited from the corresponding one in the lambda-bang calculus.
  
  
• November 28, 2022 Romain Péchoux (LORIA, U Lorraine, France): ICC@ICC: a taste of 2nd-order polytime complexity .
  
  (hide)
  After briefly introducing and describing the nature of the work done by the implicit complexity community on program complexity analysis, we will study the first (tractable and complete and) implicit characterization of the class of Basic Feasible Functionals (aka BFF, the class of second order functionals computable in polynomial time).
  
  
• October 17, 2022 Kostia Chardonnet (Université Paris Saclay and Université Paris-Cité, France): The Many-Worlds Calculus: Representing Quantum Control .
  
  (hide)
  We explore the interaction between two monoidal structures: a multiplicative one, for the encoding of pairing, and an additive one, for the encoding of choice. We propose a PROP to model computation in this framework, where the choice is parametrized by an algebraic side effect: the model can support regular tests, probabilistic and non-deterministic branching, as well as quantum branching, i.e. superposition.
  The graphical language comes equipped with a denotational semantics based on linear applications, and an equational theory. We prove the language to be universal, and the equational theory to be complete with respect to the semantics.
  
  
• October 3, 2022 Malena Ivnisky (Universidad de Buenos Aires, Argentina and Universidad de la República, Uruguay): Semántica categórica de la lógica lineal.
• September 30, 2022 Cristian Sottile (Universidad de Buenos Aires/CONICET, Argentina and UNQ, Argentina): Strong normalisation in a System F modulo isomorphisms
• September 12, 2022 Benoît Valiron (Université Paris-Saclay): LOv-Calculus: A Graphical Language for Lineal Optical Quantum Circuits.
• September 5, 2022 Rafael Romero (Universidad de Buenos Aires/CONICET, Argentina and Universidad de la República, Uruguay): Introducción a proof-nets para lógica lineal.
• August 29, 2022 Alejandro Díaz-Caro (UNQ, Argentina and ICC/CONICET, Argentina): Hacia un modelo categórico de la lógica lineal intuicionista con no-determinismo. (hide)
  
  
  (joint work with Octavio Malherbe)
  
  En [1] definimos un nuevo conectivo lógico en Deducción Natural: ⊙, el cual tiene las reglas de introducción de la conjunción y las reglas de eliminación de la disyunción, haciendo que el cut-elimination se vuelva no-determinista. A su sistema de pruebas, llamado ⊙-calculus, lo dotamos también una suma y un producto por escalar que funcionan como reglas intersticiales de la lógica (reglas que tienen la misma premisa que conclusión). En [2], extendimos la lógica lineal intuicionista con las mismas reglas intersticiales. El cálculo resultante, ℒ-calculus, mostramos que es un lenguaje donde toda lambda abstracción es una función lineal no sólo en términos semánticos, sino sintácticamente, por ejemplo, usando la suma proveniente de las reglas intersticiales, podemos demostrar que t (u+v) es equivalente a tu + tv. En [3] dimos una semántica denotacional del ℒ-calculus en la categoría de los semimódulos sobre un semianillo. En este trabajo en progreso estamos extendiendo el modelo para que sea un modelo del ℒ'⊙-calculus, es decir, la lógica lineal intuicionista extendida con reglas intersticiales y el conectivo ⊙ "linealizado". En esta charla voy a contar las dificultades para definir el modelo y las pistas que estamos siguiendo.
  
  [1] A. Díaz-Caro y G. Dowek. "A new connective in natural deduction, and its application to quantum computing" (ICTAC 2021 Best Paper Award) Lecture Notes in Computer Science 12819:175-193 https://doi.org/10.1007/978-3-030-85315-0_11, 2021.
  [2] A. Díaz-Caro y G. Dowek. "Linear Lambda-Calculus is Linear" (FSCD 2022) Leibniz International Proceedings in Informatics (LIPIcs) 228:21 https://doi.org/10.4230/LIPIcs.FSCD.2022.21, 2022
  [3] A. Díaz-Caro y O. Malherbe. "Semimodules and the (syntactically-)linear lambda calculus". arXiv:2205.02142 https://arxiv.org/abs/2205.02142, 2022 (enviado a revisión).
  
  
• August 22, 2022 Pablo Barenbaum (Universidad de Buenos Aires, Argentina and UNQ/CONICET, Argentina): Teorema de aproximación para MELL.
• August 8, 2022 Mariana Milicich (Universidad de Buenos Aires, Argentina): Licenciatura thesis defense rehearsal.
• July 11, 2022 Cristian Sottile (Universidad de Buenos Aires/CONICET, Argentina and UNQ, Argentina): Semántica de la lógica lineal con espacios de coherencia (continuación).
• July 4, 2022 Cristian Sottile (Universidad de Buenos Aires/CONICET, Argentina and UNQ, Argentina): Semántica de la lógica lineal con espacios de coherencia.
• June 27, 2022 Rafael Romero (Universidad de Buenos Aires/CONICET, Argentina and Universidad de la República, Uruguay): Conectivos aditivos y exponenciales en lógica lineal.
• June 13, 2022 Malena Ivnisky (Universidad de Buenos Aires, Argentina and Universidad de la República, Uruguay): Introducción a lógica lineal y teorema de cut elimination para MLL.
• June 6, 2022 Pablo Barenbaum (Universidad de Buenos Aires, Argentina and UNQ/CONICET, Argentina): Revisión del cálculo de secuentes y teorema de cut elimination para LK.
• May 30, 2022 Alejandro Díaz-Caro (UNQ, Argentina and ICC/CONICET, Argentina): Un nuevo conectivo lógico para computación cuántica.
• May 23, 2022 Mariana Milicich (Universidad de Buenos Aires, Argentina): Semántica denotacional para un cálculo funcional-lógico.
• May 16, 2022 Cristian Sottile (Universidad de Buenos Aires/CONICET, Argentina and UNQ, Argentina): Normalizando fuerte: clásico, polimórfico y basado en eliminadores
• May 9, 2022 Antonio Bucciarelli (IRIF, Université Paris Cité, France): Generalized Boolean algebras and clone algebras. (hide)
  
  
  The functional composition f(g_1 , . . . , g_k), the substitution t[t_1 /v_1 , . . . , t_k /v_k] of the terms t_j ’s for the variables v_j ’s in the term t, the statement case(v, v_1 , . . . , v_k ) returning one of v_j ’s depending on the value of v, are all instances of a unique (k+1)-ary operation, q(x, y_1 , . . . , y_k ), equipped with a set of k constants, representing projections, variables and (generalised) truth-values, respectively. This observation is at the root of some recent developements, at the frontier between universal algebra and computer science. I will present two of them: the k-dimensional generalisations of Boolean algebras and propositional calculus, and the purely algebraic presentation of the notion of clone.
  
  
• May 2, 2022 Rafael Romero (Universidad de Buenos Aires/CONICET, Argentina and Universidad de la República, Uruguay): Codificando programas cuánticos en diagramas SZX (hide)
  
  
  (joint work with Agustín Borgna)
  
  The Scalable ZX-calculus is a compact graphical language used to reason about linear maps between quantum states. These diagrams have multiple applications, but they frequently have to be constructed in a case-by-case basis. In this work we present a method to encode quantum programs implemented in a fragment of the linear dependently-typed Proto-Quipper-D language as families of SZX-diagrams. We define a subset of translatable Proto-Quipper-D programs and show that our procedure is able to encode non-trivial algorithms as diagrams that grow linearly on the size of the program.
  
  
• April 25, 2022 Malena Ivnisky (Universidad de Buenos Aires, Argentina and Universidad de la República, Uruguay): Dificultades para agregar punto fijo a un lambda cálculo cuántico con matrices de densidad.
• April 18, 2022 Pablo Barenbaum (Universidad de Buenos Aires, Argentina and UNQ/CONICET, Argentina): A Constructive Logic with Classical Proofs and Refutations.
• July 8, 2021 Malena Ivnisky (Universidad de Buenos Aires, Argentina): A finite-dimensional model for affine, linear quantum lambda calculi with general recursion. (hide)
  
  
  (joint work with Alejandro Díaz-Caro, Hernán Melgratti, and Benoît Valiron)
  
  We introduce 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 information and probabilistic 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 quantum lambda calculi featuring recursion with intuitionistic arrows, our model is finite-dimensional and does not need more than cones of positive matrices and affine arrows.
  
  Draft available here.
  
  
• June 24, 2021 Daniel Ventura (Universidade Federal de Goiás, Brazil): Skeletons Out! The Spirit of Node Replication. (hide)
  
  
  (joint work with Delia Kesner and Loïc Peyrot)
  
  In this talk we introduce a term calculus implementing higher-order node replication, where substitution of terms are executed constructor by constructor. Besides implementing the full node replication, two evaluation strategies are considered --call-by-name and fully lazy call-by-need-- based on the key notion of skeleton, with skeleton extraction internally codified in the calculus. Observational equivalence between strategies is proved through a standard non-idempotent intersection type system.
  
  
• July 1st, 2021 Rafael Romero (Universidad de Buenos Aires, Argentina): A note on confluence in typed probabilistic lambda calculi. (hide)
  
  
  (joint work with Alejandro Díaz-Caro)
  
  On the topic of probabilistic rewriting, there are several works studying both termination and confluence of different systems. While working with a lambda calculus 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 strategies on the overall confluence in this strongly normalizing probabilistic calculus.
  
  Accepted at LSFA 2021. Available at arXiv:2106.06633.
  
  
• May 27, 2021 Andrés Viso (Software Heritage, France and UNQ, Argentina): Encoding Tight Typing in a Unified Framework. (hide)
  
  
  This 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 sense that they provide exact information about the length of normalization sequences to normal form as well as the size of these normal forms. Moreover, the length of sequences to normal forms are discriminated according to their multiplicative/exponential nature, a concept inherited from linear logic.
  
  
• May 20, 2021 Éric Tanter (Universidad de Chile, Chile): Gradualizing the Calculus of Inductive Constructions. (hide)
  
  (Joint work with M. Bertrand, K. Maillard, N. Tabareau)
  Acknowledging 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 dependent product that CIC enjoys. Beyond this Fire Triangle of Graduality, we explore the gradualization of CIC with three different compromises, each relaxing one edge of the Fire Triangle. We develop a parametrized presentation 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 interrelation between typing, conversion, and graduality. We then establish the metatheory of this cast calculus through both a syntactic model into CIC, which provides weak canonicity, confluence, and when applicable, normalization, and a monotone model that purports the study of the graduality of two of the three variants. This work informs and paves the way towards the development of malleable proof assistants and dependently-typed programming languages.
  [The talk will be on the “intro material” 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]
  
  
• May 6, 2021 Octavio Malherbe (Universidad de la República, Uruguay): Categorías indexadas, tripos y realizabilidad. (hide)
  
  En esta charla comenzaremos con una introducción a las categorí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 alto orden y nos va permitir trabajar con ciertas abstracciones de la realizabilidad clásica de Krivine denominadas Abstract Krivine Structure (AKS) y ciertas álgebras combinatorias (denominadas full adjunction ordered combinatory 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.
  
  
• April 29, 2021 Alberto Pardo (Universidad de la República, Uruguay): Formalización de una transformación entre programas seguros usando un abordaje internalista. (hide)
  
  Los lenguajes funcionales fuertemente tipados, como Haskell, OCaml, Agda o Idris, entre otros, se destacan por sus sistemas de tipos. Gracias a sus poderosos mecanismos de 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 usarlos para para representar propiedades de los datos que manipula un programa (los llamados invariantes de tipos). Más allá del impacto (y dificultad) que esto pueda implicar en la tarea de programación, un benificio importante es que los invariantes pasan a formar parte del código ordinario del programa y por lo tanto pueden ser verificados en tiempo de compilación por el chequeador de tipos del lenguaje. Es decir, sólo son aceptados aquellos programas que preservan los invariantes que tienen definidos en sus tipos. Esta metodología de programación juega un rol clave, por ejemplo, en el desarrollo de software confiable. Al momento de codificar 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 predicados 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 del 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 aquellos términos que satisfacen el invariante. En esta charla analizaremos un 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 programas seguros tipables según un sistema flow-insensitive (en el que el nivel de seguridad de las variables es fijo). Lo interesante de nuestra formalización es que está desarrollada usando el abordaje internalista.
  
  
• April 22, 2021 Beniamino Accattoli (Inria, France): The Machinery of Interaction. (hide)
  
  Girard's geometry of interaction suggests an unusual way of evaluating lambda terms, the interaction abstract machine (IAM), first studied by Mackie and Danos & Regnier in the nineties, using linear logic proof nets. In particular, the IAM does not use environments, 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 the IAM via multi types. This talk is an overview of joint works with Ugo Dal Lago and Gabriele Vanoni.
• December 17, 2020 Vincent van Oostrom (University of Innsbruck, Austria): Commutative Residual Algebras (CRAs). (hide)
  

  We present results for commutative residual algebras (A,1,/) satisfying a/1 = a, (a/b)/(c/b) = (a/c)/(b/c), (a/b)/a = 1 and a/(a/b) = b/(b/a). Every CRA has a natural order a ≤ b if a/b = 1 and a partial composition operation . satisying (a.b)/a = b and a ≤ a.b. Then:

  • if ≤ is well-founded, ≤ is a decomposition order entailing that each a has a unique decomposition a1.....an with ai indecomposable (cf. the Fundamental Theorem of Arithmetic);
  • if ≤ is well-founded, the CRA is isomorphic to the multiset CRA over indecomposables (a representation theorem);
  • a version of the inclusion/exclusion principle can be stated and proven for CRAs, entailing all versions of that principle we know of, e.g. for cardinalities, measures, multisets and both the additive and the multiplicative natural numbers;
  • assuming . is a total operation, every CRA can be embedded in a lattice ordered group by considering fractions. for instance, the multiset CRA is embedded into the signed multisets of (Blanchette, Fleury and Traytel). stated for fractions, the inclusion/exclusion principle regains its usual form;
  • CRAs are equivalent to commutivative BCK algebras with relative cancellation (Dvurecenskij and Graziano);
  • CRAs are instances of residual algebras used to characterise orthogonality in lambda calculus and term rewriting (Terese), as expressed by the second identity of CRAs (Levy's cube law).

  
  
• December 3, 2020 Giulio Manzonetto (Université Paris 13, France): About the power of Taylor expansion. (hide)
  

  The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential lambda-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in lambda-calculus that are usually demonstrated by exploiting Scott's continuity, Berry's stability or Kahn and Plotkin's sequentiality theory.

  A paradigmatic example is given by the Perpendicular Lines Lemma for the Bõhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.

• November 26, 2020 Pablo Castro (Universidad Nacional de Río Cuarto, Argentina): Cálculo de Satisfacibilidad en Lógicas Generales. (hide)
  

  Desde su introducción por Goguen and Burstall la teoría de Instituciones ha sido usada como una formulación abstracta de la teoría de modelos. Esta teoría ha sido extendida por varios autores, incluyendo José Meseguer quien introdujo las Lógicas Generales en 1989, en su artículo Meseguer complementó las teorías de Instituciones con cálculos de pruebas. En esta charla presentaré un trabajo en conjunto con Carlos Lopez Pombo, Nazareno Aguirre y Tom Maibaum en el cual describimos una contraparte semántica de las Lógicas Generales de Meseguer. El trabajo radica en la definición abstracta de cálculos de pruebas que están basados en la construcción de modelos.

• November 19, 2020 Mauricio Guillermo (Universidad de la República, Uruguay): Juegos en Realizabilidad Clásica. (hide)
  

  En 1990 T. Griffin descubre que la instrucción de control call/cc tiene el tipo ((A ⇒ B) ⇒ A) ⇒ A, fórmula que expresa la ley de Peirce. Este descubrimiento da una interpretación computacional directa para los razonamientos de lógica clásica. Varios cálculos clásicos fueron desarrollados a partir de este descubrimiento, en general en la tradición sintáctica basada en la reescritura y la correspondencia de Curry-Howard. En la tradición semántica Krivine presenta una reformulación de la realizabilidad para dar cuenta de los razonamientos clásicos.

  Una diferencia grande entre la realizabilidad intuicionista y la clásica es que, mientras la semántica de las fórmulas en realizabilidad intuicionista es en sí misma una descripción del comportamiento de los realizadores, en realizabilidad clásica este comportamiento no es explícito.

  En esta charla veremos algunas técnicas que permiten caracterizar los realizadores clásicos de una fórmula en términos de la semántica de juegos, mostrando algunos resultados.

• November 5, 2020 Lourdes del Carmen González Huesca (Universidad Nacional Autónoma de México, México): Interactive program synthesis for modal logic S4. (hide)
  

  In this talk, I will present the ongoing work to tackle the inhabitation/synthesis problem for the case of modal types in the necessity fragment of the constructive logic S4.

  Our approach is human-driven in the sense of the usual reasoning procedures of modern theorem provers by using a so-called dual-context sequent calculus, where the sequents have two contexts, originally proposed to capture the notions of global and local truths without resorting to any formal semantics.

  Joint work with Sammantha Omaña and Favio Miranda.

• October 1st, 2020 Simon Perdrix (CNRS / LORIA, France): PBS-Calculus: A Graphical Language for Coherent Control of Quantum Computations. (hide)
  

  We will present the PBS-calculus, a diagrammatic language for representing and reasoning on quantum computations involving coherent control of quantum operations. Coherent control, and in particular indefinite causal order, is known to enable multiple computational and communication advantages over classically ordered models like quantum circuits. The PBS-calculus is inspired by quantum optics, in particular the polarising beam splitter (PBS for short). We formalise the syntax and the semantics of the PBS-diagrams, and we equip the language with an equational theory, which is proved to be sound and complete: two diagrams are representing the same quantum evolution if and only if one can be transformed into the other using the rules of the PBS-calculus. Moreover, we show that the equational theory is minimal.

• September 24, 2020 Delia Kesner (Université de Paris, CNRS, IRIF et Institut Universitaire de France): Reasoning about languages with control operators. (hide)
  

  One of the most surprising examples of the proofs-as-programs paradigm is the correspondence between the Peirce Law in classical logic and the call-cc control operator in functional programming, first noticed by Griffin in 1990, and then extended by Parigot in 1992, which has introduced the lambda-mu calculus as an isomorphic term language of classical natural deduction logic.

  This talk provides some tools to reason about dynamic properties of the lambda-mu calculus.

  In the first part of the talk, we discuss how to identify programs with control operators having exactly the same reduction semantics. This is achieved by introducing a relation which is a strong bisimulation defined over a revised presentation of Parigot's lambda-mu calculus. We show that our relation is conservative with respect to Laurent's original sigma-equivalence for lambda-mu terms (which is not a strong bisimulation), still being able to characterize structural equivalence in Polarized Proof-Nets.

  In the second part of the talk, we show how to exactly measure time and space in the lambda-mu calculus. Our approach is based on typing systems equipped with non-idempotent intersection and union types, which are able to provide information about the number of evaluation steps to normal form and the size of the corresponding normal forms. These quantitative informations are measured separately, simply because the size of the result can be exponentially bigger than the number of steps. We develop our study for three well-known evaluation strategies: head, leftmost and maximal evaluation, pertaining to head, weak and strong normalization, respectively.

• September 17, 2020 Raúl Fervari (Universidad Nacional de Córdoba, Argentina): Separation logics: a modal perspective. (hide)
  

  Modal separation logics (MSL) are formalisms that have been recently proposed combining modal operators with separating connectives, both interpreted over one-dimensional Kripke models. In this way, MSL can be seen either as separation logics enriched with local operations to reason about memory states of a piece of software, or either as modal logics with global relation-changing operators (à la sabotage logic).

  In this talk we will present MSL and some of its most interesting fragments, and discuss some results about complexity, axiom systems and expressivity. We will conclude by discussing some ongoing and future lines of research.

  Some references:

  1. S. Demri and R. Fervari. On the Complexity of Modal Separation Logics. In Proceedings of Advances in Modal Logics AiML’18, pages 179-198. College Publications, 2018.
  2. S. Demri, R. Fervari and A. Mansutti. Axiomatising Logics with Separating Conjunction and Modalities. In Proc. of the 16th European Conference on Logics in Artificial Intelligence (JELIA 2019).
  3. S. Demri and R. Fervari. The Power of Modal Separation Logics.Journal of Logic and Computation (JLC), volume 29, pages 1139–1184, 2019.
  4. B. Bednarczyk, S. Demri, R. Fervari, and A. Mansutti. Modal Logics with Composition on Finite Forests: Expressivity and Complexity. In Proc. of the 35th Annual ACM/IEEE Symposium on Logic In Computer Science (LICS'20), 2020. IEEE Press, pages 167–180, 2020.
• September 10, 2020 Gilles Dowek (Inria & ENS Paris-Saclay, France): Logipedia: towards a Wikipedia of formal proofs. (hide)
  

  Formal computerized proofs are now a central tool in computer science and in mathematics. But, each system – Coq, HOL Light, Isabelle/HOL,PVS... – implements its own language and its own theory, limiting the interoperability between systems and the sustainability of these proofs. Logipedia is an, in progress, encyclopedia of formal proofs, expressed in various theories. It is based on the idea to express these theories in a new logical framework allowing bound variables, explicit proof-terms, computation rules, and peaceful co-existence of constructive and non constructive proofs.

• September 3, 2020 Hernán Melgratti (Universidad de Buenos Aires / CONICET, Argentina): Probabilistic Analysis of Binary Sessions. (hide)
  

  We study a probabilistic variant of binary session types that relate to a class of Finite-State Markov Chains. The probability annotations in session types enable the reasoning on the probability that a session terminates successfully, for some user-definable notion of successful termination. We develop a type system for a simple session calculus featuring probabilistic choices and show that the success probability of well-typed processes agrees with that of the sessions they use. To this aim, the type system needs to track the propagation of probabilistic choices across different sessions.
  Joint work with: Omar Inverso, Hernán Melgratti, Luca Padovani, Catia Trubiani, Emilio Tuosto

• August 20, 2020 Margherita Zorzi (Università di Verona, Italy): A Host-Core type theory as internal language. (hide)
  

  JOINT WORK WITH Davide Trotta Nad Roberto Giacobazzi (University of Verona).
  Programming platforms and modern IDE systems provide efficient methods to manage and control the process of software development in an heterogeneous programming language. In this context the programmer uses a main language, the host, and delegates some tasks to another one, typically domain specific, called it the core, hierarchically embedded into the former. In this paper we provide a formal characterization of host-core languages in terms of the internal language of a category. We propose HC0, a type theory able to capture the common properties of an ideal class of (functional) host-core languages. The type theory must to be “mixed”, because it has to describe both host and core syntaxes and the communication between the two parts. It is also compositional, i.e. it can be easily extended without changing its structure. We provide a denotational semantics in terms of enriched categories, and we prove a strong relationship between syntax and semantics via the internal language a notion, at the best of our knowledge, completely new in programming theory. By proving that HC0 is the internal language of the category of its models we can equivalently reason both from a syntactical and a semantical point of view. The internal language allows us to provide a formal definition of host-core language and to characterize the semantics of the class languages that follows in our definition. Moreover, we also obtain some interesting byproducts. We are able to provide a first comparison between the host-core model and the standalone one (i.e. the programming paradigm based on a single language). Finally, we define a function that, given a model (in the sense we defined for HC0) extracts a host-core type theory.

• August 13, 2020 Mauricio Ayala Rincón (Universidade de Brasília, Brazil): Termination of Functional Programs and Term Rewriting Systems. (hide)
  

  This talk will present current research on the formalization of termination for a functional language model called PVS0. This model contributes to the meta-theoretical study of the PVS higher-order logic and their computational aspects. Automation of the verification of termination increases the semantic capabilities of deductive systems and compilers and involves research challenges that range from proving fundamental theorems about the pertinence of the computational model to the integration of mechanical proofs of the correspondence of different termination criteria for computational frameworks such as PVS0 and term rewriting systems.

• August 6, 2020 Bruno Lopes (Universidade Federal Fluminense, Brazil): A logical framework to reason about Reo circuits. (hide)
  

  Reo is a graphical-based coordination modelling language which aims to capture and model the interaction between pieces of software, using structures known as channels.
  The fact that Reo can be used to model many real-world situations has attracted attention from researchers, resulting in a great effort directed in formalising means to verify properties of Reo circuits. This work presents a logical framework to model and reason about Reo circuits in a proof-theoretical way (using Coq proof-assistant), and by means of model checking (using nuXmv model checker).

• July 23, 2020 Mallku Sodevilla (Universidad Nacional de Córdoba, Argentina): Semántica operacional y su aplicación para el estudio de recolección de basura, en Lua 5.2. (hide)
  

  Lua es un lenguaje de programación imperativo de scripting, que ofrece tipado dinámico, manejo automático de memoria, facilidades para la descripción de datos, y mecanismos de meta-programación para adaptar el lenguaje a dominios específicos. Es utilizado en proyectos de diversa naturaleza, desde desarrollo de juegos, de manera notable en juegos "AAA", desarrollo de plugins, firewall de aplicaciones web, y en sistemas embebidos. Gracias al éxito de Lua es posible encontrar diversas implementaciones alternativas y analizadores estáticos. Sin embargo, la naturaleza informal de la especificación del lenguaje implica que quienes desarrollan esas herramientas no pueden proveer garantías formales de corrección para las mismas.

  En este trabajo presentamos una formalización de la semántica operacional de Lua 5.2, incluyendo recolección de basura (GC) y sus interfaces (finalizadores y tablas débiles; una forma de implementar referencias débiles). Validamos la semántica mediante su mecanización, utilizando PLT Redex, y el testeo de la misma con respecto a la suite de tests del intérprete oficial de Lua. A su vez, utilizamos las facilidades ofrecidas por PLT Redex para la mecanización de sistemas formales y testeo aleatorio de propiedades, para obtener evidencia de la propiedad de progreso de la semántica. Para GC proveemos un framework para razonar formalmente sobre propiedades de cualquier algoritmo de GC basado en un criterio sintáctico. Dentro del framework podemos formalizar y esbozar la demostración de propiedades sobre GC, incluyendo su corrección (sin considerar sus interfaces).

• July 16, 2020 Miguel Pagano (Universidad Nacional de Córdoba, Argentina): Realizabilidad para Adecuación de la máquina de Sestoft. (hide)
  

  Desde hace unos 10 años que se usa biortogonalidad (una forma de definir relaciones lógicas) para probar la corrección de compiladores para lenguajes funcionales. En esta charla contaré el trabajo que venimos realizando en Córdoba hacia una adaptación de esa técnica para un lenguaje lazy. Es un trabajo conjunto que empezó Leo Rodríguez con Daniel Fridlender, luego nos sumamos con Ale Gadea.

• July 2, 2020 Benoît Valiron (LRI / CentraleSupélec, France): Towards a Curry-Howard Isomorphism for quantum control. (hide)
  

  In this talk, I will present a linear and reversible language with inductive and coinductive types, together with a Curry-Howard correspondence with the logic muMALL : linear logic extended with least and greatest fixed points which allow inductive and coinductive statements. We shall discuss the language, the correspondance with logic, and the possible extensions to quantum control of the approach.

• June 25, 2020 Daniele Nantes (Universidade de Brasília, Brazil): An Investigation of Linear Substitution Lambda-Calculus as Session-Typed Processes. (hide)
  

  Sandra Alves, Daniele Nantes, J. A. Pérez and Daniel Ventur
  
  Abstract. This work in progress investigates a type directed encoding of the simply-typed linear substitution lambda-calculus to session-typed pi-processes, taking into account an operational semantics defined by a linear weak head reduction strategy. The encoding adapts the one by Toninho et. al., which encodes the simply-typed lambda-calculus into a session-typed pi-calculus through linear logic, while extending it to explicit substitutions, considering a generalisation of the pi-calculus operational semantics with reduction rules at a distance, as proposed by Accattoli. These changes, while weakening the simulation of lambda-calculus in the pi-calculus, when compared with the 1-to-1 simulation obtained by Accattoli, allow for an as tight as possible encoding of well-typed functions as session-typed processes.

• June 18, 2020 Eduardo Bonelli (Stevens Institute of Technology, United States): Logic of Proofs y Lambda Cálculo: proofs terms y unificación de alto-orden . (hide)
  

  Logic of Proofs (LP) [Art94] es la primera de una familia de lógicas modales hoy conocidas como Justification Logics. LP incluye proposiciones de la forma [s]A donde "s" denota la razón or justificación de la veracidad de A. Si uno se "olvida" la razón "s" en la proposición [s]A, queda el operador modal []A de la lógica modal S4.

  En esta charla vamos a explorar dos lazos entre LP y lambda cálculo:

  1. El primero se podría resumir como:
         [s]A es el tipo de los computaciones o proof terms con source s
     Un proof term es una expresión que denota una computación o derivación desde un término source a un término target (Ej. capítulo 8 del TERESE para TRS).
      
  2. El segundo de podría resumir como:
         La decoración de pruebas de S4 para obtener pruebas de LP se reduce a un problema de unificación de alto-orden.
• June 4, 2020 Pablo Barenbaum (Universidad de Buenos Aires, Argentina): Un cálculo-lambda relacional. (hide)
  

  La programación relacional se caracteriza por el hecho de que las expresiones representan relaciones que no tienen por qué ser funcionales, y por el papel fundamental que desempeña la unificación en el modelo de cómputo. Uno de sus exponentes más puros es el lenguaje de programación miniKanren. En esta charla presentaremos una variante del cálculo-lambda extendido con construcciones propias de la programación relacional: alternativa no deterministica, secuenciación explícita y unificación. Discutiremos diversos aspectos de este cálculo actualmente en desarollo: semántica operacional, denotacional e implementación de un lenguaje de programación basado en estos principios.

• September 10, 2019. Pierre Vial gives an overview on his work with a talk entitled An introduction to idempotent or not intersection types
• July 8, 2015. Abuzer Yakaryilmaz gives some insight on his research line with his talk entitled Classical and Quantum Automata on Promise Problems
• April 22, 2015. Andrés Viso gives us an overview on his joint work with Eduardo Bonelli and Mauricio Ayala-Rincon entitled Static Typing for Path Polymorphism
• February 18, 2015. Bernard Serpette gives some insight on his recent work entitled Computing with collaborative side effects
• November 26, 2014. Nicolás Passerini and Pablo Tesone introduce us to their recent work on An Extensible Constraint-based Type Inference Algorithm for Object-Oriented Dynamic Languages Supporting Blocks and Generic Types
• November 12, 2014. Jose Santos tells us about his work on information flow analysis entitled Enforcing Secure Information Flow in Client-side Web Applications.
• October 29, 2014. Carlos Lombardi gives some insight on his PhD thesis entitled Reduction Space for Non-Sequential and Infinitary Rewriting Systems.
• October 1 & 15, 2014. Alejandro Díaz-Caro tells us about his joint work with Gilles Dowek on Type Theory Modulo Isomorphism
• September 3 & 17, 2014. Andrés Viso introduces us to some of the details on proving Strong Normalization for CPP, a type system for a pattern calculus supporting Path Polymorphism. Joint work with Eduardo Bonelli and Mauricio Ayala-Rincón.
• August 20, 2014. Thibaut Balabonski opens this new semester's seminar at UNQ with his talk on Semantic Proofs of Correctness For Low-level Concurrent Program Optimisations
• June 13, 2014. Eduardo Bonelli presents us to some recent work by Beniamino Accattoli and Ugo Dal Lago entitled Beta Reduction is Invariant, Indeed.
• May 29, 2014. Pablo Barenbaum give us some insight on his recent joint work with Eduardo Bonelli on Optimal Reduction in the Linear Substitution Calculus.
• May 13, 2014. Antonio Bucciarelli joins us for a lecture on Definability and Full Abstraction Problems for Lambda Calculi.
• March 27, 2014. Andrés Viso gives us an overview on his joint work with Eduardo Bonelli and Mauricio Ayala-Rincon entitled Typing a Calculus of Patterns Supporting Path Polymorphism.
• August 23, 2013. Ioana Cristescu presents her joint work with Jean Krivine and Daniele Varacca entitled A Compositional Semantics For The Reversible Pi-calculus.
• July 25, 2013. Jean-Jacques Lévy revisits his recent talk Understanding Strong Normalisation on his visit to Buenos Aires.
• June 27, 2013. Beta Ziliani visits Buenos Aires and tells us about his recent work on extending Coq with Mtac: a Monad for Typed Tactic Programming.
• June 6, 2013. Andrés Viso gives us a brief introduction on Typing Systems for different Pattern Calculi. The talk is based on Barry Jay's book Pattern Calculus: Computing with Functions and Structures.
• May 16, 2013. Delia Kesner gives us an overview on her joint work with Antonio Bucciarelli and Simona Ronchi della Rocca entitled Observability Through Product Types.
• May 9, 2013. Carlos Lombardi introduces us to the theory of Proof Terms as a continuation of his previous talk on equivalences between reductions for Infinitary Rewriting Systems. Further information is available on Term Rewriting Systems (TeReSe) chapter 8.
• April 25, 2013. Gabriela Steren gives us an overview on her work Intuitionistic Hypothetical Logic of Proofs presented on The 6th Workshop on Intuitionistic Modal Logic and Applications (IMLA 2013) last April 7.
• April 11, 2013. Carlos Lombardi introduces us to Infinitary Rewriting Systems and shows some interesting equivalences between reductions. Background information can be found on Term Rewriting Systems (TeReSe) chapter 12 and Infinitary Normalization by Jan Willem Klop and Roel De Vrijer.

Recent and upcoming events

• August 12-23, 2024 Alejandro Díaz-Caro will be at Universidad de la República, working with Octavio Malherbe.
• July 29-August 8, 2024 ECI 2024 will be held at Universidad de Buenos Aires, chaired by Pablo Barenbaum.
• July 15-19, 2024 QPL 2024 will be held at Buenos Aires, chaired by Alejandro Díaz-Caro.
• July 1-5, 2024 Pablo Barenbaum, Alejandro Díaz-Caro, Malena Ivnisky, Rafael Romero, and Cristian Sottile will participate as speakers from the 20th Latin American Symposium on Mathematical Logic, at Montevideo, Uruguay
• June 26th, 2024 Jornada LoReL 2024 takes place at ICC (Exactas-UBA)

• June 1st, 2024 A Marie Sklodowska-Curie Action "Staff Exchanges" grant has been awarded to several members of the QuICC team, involving 12 participating institutions from Argentina, Uruguay, France, and Italy. The project, called QCOMICAL: Quantum Computing and Its Calculi, is set to start in December 2024 and will run for 4 years.
• May 11 to June 9, 2024 Alejandro Díaz-Caro is visiting Université Paris-Saclay, as an invited profesor by CentraleSupélec, to work with Benoît Valiron and Vladimir Zamdzhiev from the Quacs team, and Gilles Dowek from the Deducteam team.
• February 21, 2024 Giselle Zeitoune defends her Licenciatura thesis at Universidad de Buenos Aires, supervised by Pablo Barenbaum.
• February, 2024 Alejandro Díaz-Caro visits Universidad de la República, to work with Octavio Malherbe.
• December 20, 2023 Martín Villagra defends his Licenciatura thesis at Universidad de Rosario, supervised by Alejandro Díaz-Caro and Pablo E. Martínez López.
• November 13 to December 17, 2023 Alejandro Díaz-Caro will be at LORIA as "invited researcher", working with the team Moqcua.
• August 28 to September 9, 2023 Alejandro Díaz-Caro is at Universidad de la República, working with Octavio Malherbe.
• August 3, 2023 Nicolás San Martín defends his Licenciatura thesis at Universidad de Buenos Aires, supervised by Alejandro Díaz-Caro.
• July, 2023. Pablo Barenbaum gives a talk as invited speaker at LSFA 2023.
• June 22 to July 21, 2023. Alejandro Díaz-Caro is at INRIA as "invited professor", working with the teams QuACS, and DEDUCTEAM.
• April/May, 2023. Alejandro Díaz-Caro is at CentraleSupélec as "invited professor", working with the teams QUACS, and DEDUCTEAM.
• March, 2023. Alejandro Díaz-Caro is at Universidad de la República, working with Octavio Malherbe.
• October 26, 2022. Alejandro Díaz-Caro gives a talk at JCC 2022. Universidad Nacional de Rosario.
• August 10, 2022. Mariana Milicich defends her Licenciatura thesis at Universidad de Buenos Aires, supervised by Pablo Barenbaum.
• August, 2022. Malena Ivnisky participates of FLoC as student volunteer.
• June/July, 2022. Alejandro Díaz-Caro visits the LMF lab to work with Benoît Valiron and LORIA to work with Simon Perdrix.
• May 12, 2022. Mariana Milicich has been granted a scholarship from the FSMP (MathInParis2022), to do her PhD under the direction of Pablo Barenbaum and Delia Kesner, jointly between Université Paris Cité and UBA, starting in September 2022.
• April 25-May 6, 2022. Alejandro Díaz-Caro visits Universidad de la República to work with Octavio Malherbe.
• March 28-April 7, 2022. Alejandro Díaz-Caro visits Universidad de Chile to work with Federico Olmedo.
• November 5, 2021. Teodoro Freund defends his Licenciatura thesis at Universidad de Buenos Aires, supervised by Pablo Barenbaum.
• November 2021. Alejandro Díaz-Caro, Malena Ivnisky, and Rafael Romero visits the LMF at Paris-Saclay to work with Gilles Dowek, Benoît Valiron and Agustín Borgna financed by ECOS-Sud and the IRP SINFIN.
• October 29, 2021. Cristian Sottile gives a talk at 50 JAIIO at the EST symposium about his Master's thesis.
• October 14, 2021. Alejandro Díaz-Caro gives a talk at the 106 Reunión Anual de Física (RAFA) at the Fundamentos e Información Cuántica Division.
• September 24, 2021. Hernán Melgratti, CONICET researcher at ICC and Professor at UBA, joins LoReL team.
• September 23, 2021. Pablo Barenbaum is selected as CONICET researcher within LoReL at Universidad Nacional de Quilmes.
• September 21, 2021. Alejandro Díaz-Caro and Mauro Jaskelioff obtained a PIP-CONICET project for the period 2021-2023.
• September 10, 2021. Alejandro Díaz-Caro and Gilles Dowek won the Best Paper Award (first place shared with another work) at ICTAC 2021 for their paper A New Connective in Natural Deduction, and its Application to Quantum Computing.
• July 2021. Alejandro Díaz-Caro has been elected member of the Steering Committee of FSCD for the period 2021-2024.
• June 4, 2021. Rafael Romero and Alejandro Díaz-Caro got a presentation accepted at LSFA 2021.
• May 29 2021. Malena Ivnisky got a presentation accepted at Women in Logic 2021.
• May 17 2021. Malena Ivnisky and Alejandro Díaz-Caro, toghether with Hernán Melgratti and Benoît Valiron, got a presentation accepted at TYPES 2021.
• May 7 2021. Alejandro Díaz-Caro got two presentations accepted at QPL 2021, one with Octavio Malherbe and one with Gilles Dowek.
• April 20, 2021. Federico Lochbaum defends his Licenciatura thesis at Universidad Nacional de Quilmes, supervised by Pablo Barenbaum.
• April 15, 2021. Alejandro Díaz-Caro gives an invited talk at LSFA 2021.
• April 13, 2021. Cristian Sottile gives a talk at Midlands Graduate School 2021.
• February 27, 2021. Malena Ivnisky, Rafael Romero, and Cristian Sottile presents their recent works at JIF 2021 on March 25-27, 2021.
• February 12, 2021. A new project PICT has been granted for the period 2021-2023. Directed by Federico Holik, and with Alejandro Díaz-Caro as a member.
• December 13, 2020. Mariana Milicich has been granted with a scholarship for the Computer Science department at UBA to do a new intership within LoReL, under the mentorship of Pablo Barenbaum.
• December 10, 2020. A new cooperation project has been stablished between LoReL members and Chile, Uruguay, and France. STIC-AmSud Project 21STIC10 "Qapla'". 2021-2022.
• December 1, 2020. Malena Ivnisky has been granted with a UBA scholarship to do her PhD thesis at UBA within LoReL, under the direction of Alejandro Díaz-Caro and Octavio Malherbe, starting in December 2020.
• November 20, 2020. Pablo Barenbaum defends his PhD thesis entitled "Semántica dinámica de cálculos de sustituciones explícitas a distancia".
• October 15, 2020. Alejandro Díaz-Caro gives an interview to the radio show "El Faro - Un programa de ciencia" (FM Radio Noticias, Santa Rosa, La Pampa).
• September 4, 2020. Cristian Sottile gives a talk at IFL 2020 (joint work with Alejandro Díaz-Caro and Pablo E. Martínez López).
• September 1st, 2020. Alejandro Díaz-Caro gives a talk at the seminar of the QuICC Team.
• August 28, 2020. Malena Ivnisky defends her Licenciatura thesis (eq. Masters in the EU) at Universidad de Buenos Aires, supervised by Alejandro Díaz-Caro and Hernán Melgratti.
• August 17, 2020. Cristian Sottile gives a talk at the Scottish Programming Languages and Verification Summer School 2020.
• July 23, 2020. Alejandro Díaz-Caro gives a talk at "Lógicos em Quarentena" seminar of the Brazilian Logic Society.
• July 22, 2020. Andrés Viso defends his PhD thesis at Universidad de Buenos Aires, which has been supervised by Eduardo Bonelli and Delia Kesner.
• May 18, 2020. Alejandro Díaz-Caro becomes the new director of LoReL, after many years of the direction of Eduardo Bonelli and Alejandro Ríos.
• May 12, 2020. Alejandro Díaz-Caro gives a talk at FICH-UNL invited by the students union.
• May 4, 2020. Francisco Noriega defends his Licenciatura thesis (eq. Masters in the EU) at Universidad de Buenos Aires, supervised by Alejandro Díaz-Caro.
• April 1, 2020 Rafael Romero and Cristian Sottile officially start their PhD fellowships.
• March 19, 2020. Rafael Romero defends his Licenciatura thesis (eq. Masters in the EU) at Universidad de Buenos Aires, supervised by Alejandro Díaz-Caro.
• March 10, 2020. Cristian Sottile defends his Licenciatura thesis (eq. Masters in the EU) at Universidad Nacional de La Plata, supervised by Alejandro Díaz-Caro and Pablo E. "Fidel" Martínez López.
• January 15, 2020. Cristian Sottile has been granted with a CONICET scholarship to do his PhD thesis at UBA within LoReL, under the direction of Alejandro Díaz-Caro and Pablo E. Martínez López, starting in April 2020.
• January 15, 2020. Lucas Rafael Romero has been granted with a CONICET scholarship to do his PhD thesis at UBA within LoReL, under the direction of Alejandro Díaz-Caro and Octavio Malherbe, starting in April 2020.
• October 11, 2019. Alejandro Díaz-Caro gives a seminar at BA-Logic.
• September 13, 2019. Pierre Vial gives a seminar at ICC.
• September 12, 2019. Alejandro Díaz-Caro gives a science popularization talk about quantum computing at Semana de la computación. Exactas-UBA.
• September 8 to 22, 2019. Alejandro Ríos visits Antinio Bucciarelli and Delia Kesner at IRIF, France.
• September 5 to October 5, 2019. Andrés Viso visits Antinio Bucciarelli and Delia Kesner at IRIF, France.
• September 2 to 6, 2019. Alejandro Díaz-Caro visits Octavio Malherbe at UdelaR, Uruguay.
• August 20, 2019. The eighth LoCIC meeting is taking place at FI-UBA.
• August 1st, 2019. Agustín Borgna defends his Licenciatura thesis (eq. Masters in the EU) at Universidad de Buenos Aires, supervised by Alejandro Díaz-Caro.
• July 2, 2019. ICC has been chosen to organize FSCD 2021. Alejandro Díaz-Caro is the chair of the organisation committee.
• June 19, 2019. Alejandro Díaz-Caro visits Delia Kesner and Beniamino Accattoli at IRIF, France.
• June 17, 18, 20, and 21, 2019. Alejandro Díaz-Caro visits Gilles Dowek at LSV, France.
• June 11 to 14, 2019. Alejandro Díaz-Caro visits Benoît Valiron at LRI, France.
• May 22 to 24, 2019. The second FunLeP meeting is taking place at UNQ.
• May 14 to 17, 2019. Alejandro Díaz-Caro visits Alexandre Miquel and Benoît Valiron (who is visiting) at Universidad de la Repúbica, Montevideo, Uruguay.
• May 2nd, 2019. We have a day of LoReL team, with talks by all the Ph.D. and Masters students.
• April 9 to 14, 2019. Alejandro Díaz-Caro visits Octavio Malherne at Universidad de la Repúbica, Montevideo, Uruguay.
• March 15th, 2019. Alejandro Díaz-Caro and Pablo Barenbaum give talks at the ICC day, Buenos Aires, Argentina.
• March 13th, 2019. Alejandro Díaz-Caro gives a talk at the V International Workshop on Quantum Mechanics and Quantum Information: Physical, Philosophical and Logical Perspectives at Universidad CAECE, Buenos Aires, Argentina.
• February 18 to 22, 2019. Alejandro Díaz-Caro gives a talk and a mini-course at the XI Summer Workshop in Mathematics at Universidade de Brasília, Brazil.
• January 16 to 27, 2019. Alejandro Díaz-Caro visits Federico Olmedo at Universidad de Chile, Santiago, Chile.
• December 3 to 20, 2018. Alejandro Díaz-Caro visits Gilles Dowek at ENS Paris-Cachan and Benoît Valiron at Université Paris-Sud, France.
• November 22, 2018. Alejandro Díaz-Caro gives a talk at the VIII Conference on Quantum Foundations: Quantum Logic & Quantum Structures, held at CAECE, Buenos Aires, Argentina.
• November 17 to December 16, 2018. Andrés Viso visits Delia Kesner and Antonio Bucciarelli at IRIF, Université Paris Diderot, France.
• November 17 to 30, 2018. Alejandro Ríos visits Delia Kesner and Antonio Bucciarelli at IRIF, Université Paris Diderot, France
• November 15, 2018. Malena Ivnisky gives a talk at a Master's seminar event at LRI about her master's thesis, France.
• November 12 to 24, 2018. Malena Ivnisky visits Benoît Valiron at Université Paris-Sud, France.
• October 27 to 30, 2018. Alejandro Díaz-Caro visits Octavio Malherbe at Universidad de la República, Uruguay.
• September 6, 2018. 6ta Jornada de Lógica, Computación e Información Cuántica takes place at ICC (Exactas-UBA).
• August 17, 2018. 1er Encuentro de Fundamentos de Lenguajes de Programación (FunLeP) takes place at CIFASIS (Rosario). LoReL members are part of FunLeP organisation.
• July 2-16, 2018. Alejandro Díaz-Caro visits Marcos Villagra at NIDTEC, Universidad Nacional de Asunción, Paraguay.
• June 28, 2018. Gonzalo Ciruelos defends his licenciatura thesis (eq. masters in the eu) at universidad de buenos aires, supervised by Pablo Barenbaum.
• June 27, 2018. Juan Pablo Rinaldi defends his Licenciatura thesis (eq. Masters in the EU) at Universidad Nacional de Rosario, supervised by Alejandro Díaz-Caro.
• May 21, 2018. The Logic and Foundations of Programming Languages Day takes place at Exactas-UBA.
• April 5, 2018. Agustín Borgna gives a seminar at Deducteam at LSV, ENS Paris-Saclay, Cachan, France.
• April 2 to 6, 2018. Alejandro Díaz-Caro visits Deducteam at LSV, ENS Paris-Saclay, Cachan, France.
• March 26 to 30, 2018. Alejandro Díaz-Caro visits ModHel at LRI Université Paris-Saclay, Orsay, France.
• March 19 to 22, 2018. Alejandro Díaz-Caro gives a seminar at CVQT in Edinburgh, UK.
• March 9, 2018. Alejandro Díaz-Caro gives a seminar at WTPC in UNQ.
• March 1, 2018. 4ta Jornada de Lógica, Computación e Información Cuántica takes place at UNQ.
• December, 2017. Alejandro Díaz-Caro visits LSV at ENS-Cachan, Paris.
• November, 2017. Andrés Viso visits IRIF at Université Paris Diderot, Paris.
• October 25-27, 2017. Alejandro Díaz-Caro gives a seminar at the XV JCC in Rosario.
• October 19, 2017. LIA INFINIS workshop takes place at UBA.
• August, 2017. Pablo Barenbaum visits Stevens Institute of Technology in Hoboken, NJ.
• July 24-29, 2017. Alejandro Díaz-Caro gives a course at the ECI 2017 in Buenos Aires.
• April 25, 2017. Alejandro Díaz-Caro gives a seminar in the IFLP, La Plata.
• April 20-21, 2017. Alejandro Díaz-Caro visits at Facultad de Ingeniería (UdelaR), Montevideo.
• April 3-12, 2017. Alejandro Díaz-Caro visits at ENS-Cachan, Paris.
• March 23, 2017. Jornada de lógica, computación e información cuántica takes place at UNQ.
• December 5-6, 2016. FoQCoSS Kickoff Workshop takes place at UNQ.
• October 2016. Alejandro Díaz-Caro gives a course at CACIC 2016 in San Luis.
• Jan/Dec 2016. Eduardo Bonelli stays at the Stevens Institute of Technology as an invited professor.
• May 2016: Alejandro Díaz-Caro visits ENS-Cachan, Paris.
• Jan/Jul 2016. Alejandro Díaz-Caro stays at Università di Torino as an invited professor.
• December 17, 2015. Juan Edi defends his Licenciatura thesis (eq. Masters in the EU) at Universidad de Buenos Aires, supervised by Andrés Viso and Eduardo Bonelli.
• October 2015. Pablo Barenbaum visits PPS Laboratoire in Paris.
• July 17. LIA INFINIS workshop takes place at UBA.
• July 2015. Thibaut Balabonski visits Buenos Aires.
• July 2015. Abuzer Yakaryilmaz visits UBA for a course at the ECI 2015 Winter School, and gives a seminar at UNQ.
• May/Jun 2015. Andrés Viso visits PPS Laboratoire in Paris.
• Feb/Mar 2015. Bernard Serpette visits Buenos Aires.
• Feb/May 2015. Pablo Barenbaum visits PPS Laboratoire in Paris.
• February 2015. Alejandro Díaz-Caro gives the course at RIO 2015 in Río Cuarto.
• December 15, 2014. Gabriela Steren presents her PhD thesis at UBA.
• November 7, 2014. Carlos Lombardi presents his PhD thesis at UBA.
• November 5-6, 2014. Delia Kesner visits Buenos Aires.
• November 2014. Jose Santos visits Buenos Aires.
• August, 2014. Thibaut Balabonski visits Buenos Aires.
• July 2014. Beta Ziliani gives a course on Coq at the ECI 2014 Winter School at UBA.
• November 2013. Mauricio Ayala-Rincón visits Buenos Aires.
• October 2013. Delia Kesner visits UBA.
• Sept/Oct 2013. Roel de Vrijer visits UBA.
• July 2013. Jean-Jacques Lévy gives a course on Reductions and casualty in the ECI 2013 Winter School at UBA.
• May 2013. Delia Kesner visits UBA.
• 11 April 2013. First meeting of LoReL seminar at UBA.
• February 2013. Pierre Lescanne visits UBA in February 2013.
• 9-11 Oct 2012. Beniamino Accattoli gives a short course on Linear Logic, Lambda-calculus, and Explicit Substitutions.
• 03 Oct 2012. Mini Workshop on Rewriting and Type Theory takes place at UBA.
• 01 Oct 2012. INFINIS Business meeting takes place at UBA.
• October 2012. Roel de Vrijer visits Buenos Aires.
• October 2012. Delia Kesner and Beniamino Accatolli visits Buenos Aires.
• August 2012. Mauricio Ayala-Rincón visits UNQ in the context of a STIC-AmSud cooperation project.
• 07 Sep 2012. Carlos Lombardi gives a talk at INFINIS Meeting.
• 03 Sep 2012. Eduardo Bonelli gives a talk at WoLLIC 2012, Sep 3-6, 2012.
• 29 May 2012. Delia Kesner presents a joint paper at RTA 2012.
• 22-23 May 2012. Eduardo Bonelli gives a 4 hour short course on Normalisation for Dynamic Pattern Calculi at Universidad de Brasilia.

Recent and upcoming visitors

• August, 2024. Giulio Guerrieri (University of Sussex, UK).
• March, 2024. Delia Kesner (U. Paris-Cité, France).
• January, March, and May 2024. Octavio Malherbe (UdelaR, Uruguay).
• December, 2023. Giulio Guerrieri (Aix-Marseille U., France).
• November, 2023. Pablo Arrighi (U. Paris-Saclay, LMF, France).

• March, April, August, and October 2023. Octavio Malherbe (UdelaR, Uruguay).
• March 2023. Delia Kesner (U. Paris-Cité, France).
• December 2022. Agustín Borgna (U Paris-Saclay & U Lorraine, France).
• November-December 2022. Delia Kesner (U. Paris-Cité, France).
• November-December 2022. Romain Péchoux (LORIA, U Lorraine, France).
• October 2022. Kostia Chardonnet (LMF, Paris-Saclay, France).
• September 2022. Benoît Valiron (LRI, CentraleSupélec, Francia).
• July-August 2022. Giuseppe Di Molffeta (Aix Marseille Université, Francia).
• April-May 2022. Antonio Bucciarelli (IRIF, U Paris, Francia).
• March, September, and November 2022. Octavio Malherbe (UdelaR, Uruguay).
• February 2022. Federico Olmedo (U de Chile, Chile).
• January 2022. Agustín Borgna (U Paris-Saclay & U Lorraine, France).
• January 2022. Simon Perdrix (CNRS & U Lorraine, France).
• December 2021. Octavio Malherbe (UdelaR, Uruguay).
• November 2021. Delia Kesner (IRIF, U Paris, France).
• November 2021. Gilles Dowek (Inria, U Paris-Saclay, France).
• December 16-20, 2019 and February 18-22, 2020. Octavio Malherbe.
• November 26 to December 6, 2019. Gilles Dowek.
• November 13-22, 2019. Simon Perdrix.
• November 8-22, 2019. Delia Kesner.
• October 14-25, 2019. Ivan Marquez.
• September 9 to October 4, 2019. Pierre Vial.
• August 20 to September 30, 2019. Nely Plata-César.
• July 22-27, 2019. Pablo Arrighi and Beniamino Accattoli.
• July 1st to 12, 2019. Federico Olmedo.
• April 26-29, 2019. Octavio Malherbe.
• April 8-22, 2019. Delia Kesner and Antonio Bucciarelli
• March 11-14, 2019. Marcos Villagra.
• February 26 to March 1, 2019. Octavio Malherbe.
• September 20-23, 2018. Octavio Malherbe.
• September 6, 2018. Marcos Villagra and Alexandre Miquel.
• September 1-11, 2018. Delia Kesner.
• July 23 to August 3, 2018. Gilles Dowek.
• June 16-19, 2018. Octavio Malherbe.
• May 18-22, 2018. Alexandre Miquel and Mauricio Guillermo.
• May 14-27, 2018. Delia Kesner and Antonio Bucciarelli.
• May 14-25, 2018. Benoît Valiron.
• April 19-22, 2018. Octavio Malherbe.
• January 22-26, 2018. Octavio Malhebre.
• November 8-9, 2017. Marcos Villagra.
• October 12-15, 2017. Octavio Malherbe.
• September 13-22, 2017. Delia Kesner.
• July 10-21, 2017. Simon Perdrix.
• June 22-30, 2017. Gilles Dowek.
• May 4-14, 2017. Delia Kesner.
• March 23-26, 2017. Octavio Malherbe.
• December 2016. Gilles Dowek, Pablo Arrighi, Simon Martiel, Stefano Facchini, Benoît Valiron, Renaud Vilmart, Octavio Malherbe.
• April 2016. Delia Kesner.
• July 2015. Abuzer Yakaryilmaz and Thibaut Balabonski.
• Feb/Mar 2015. Bernard Serpette.
• November 5-6, 2014. Delia Kesner.
• November 2014. Jose Santos.
• September 2014. Delia Kesner.
• August 2014. Thibaut Balabonski.
• May 5-16, 2014. Delia Kesner and Antonio Bucciarelli.
• November 2013. Mauricio Ayala-Rincon.
• October 2013. Delia Kesner visited UBA.
• Sept/Oct 2013. Roel de Vrijer visited UBA.
• July 2013. Jean-Jacques Lévy visited UBA for a course in the ECI 2013.
• May 2013. Delia Kesner.
• February 2013. Pierre Lescanne. He also gave a course in the Río Cuarto summer school.
• October 2012. Roel de Vrijer.
• August 2012. Mauricio Ayala Rincón visited UNQ during the end of August 2012 for two weeks in the context of a STIC-AmSud cooperation project.

Current projects

1. HORIZON-MSCA-2023-SE 101182520. QCOMICAL: Quantum Computing and Its Calculi. European Commission. 2025-2028.
2. CNRS IRP SINFIN: Systems, verIfication, computiNg Foundations, logIque, laNguages. CNRS-CONICET. 2024-2029.
3. PICT-2021-I-A-00090. Computación cuántica y sus cálculos. MinCyT. 2023-2026.
4. PICT-2021-I-INVI-00602. Tipos cuantitativos para lenguajes de programación. MinCyT. 2023-2024.
5. PICT 2019-1272. Estructuras lógicas y algebraicas vinculadas al procesamiento de la información cuántica. MinCyT. 2021-2024.
6. PIP 11220200100368CO. Fundamentos de lenguajes para computación cuántica y consecuencias en sistemas clásicos. CONICET. 2021-2023.
7. PUNQ 2218/22. Fundamentos de lenguajes de programación: sistemas de pruebas y computación cuántica. Universidad Nacional de Quilmes. 2022-2025.
8. PUNQ 2219/22. Diseño de lenguajes de programación: fundamentos e impacto en didáctica. Universidad Nacional de Quilmes. 2022-2025.

Past projects

1. STIC-AmSud. Qapla' - Quantum Aspects of Programming Languages. Argentina: Universidad Nacional de Quilmes and Universidad de Buenos Aires. Brazil: Universidade Federal de Santa Maria. France: INRIA, CNRS/LORIA, Université Aix-Marseille, CentraleSupélec/LRI. Chile: Universidad de Chile. Uruguay: Universidad de la República. 2021-2022.
2. PUNQ 1342/19. Fundamentos de lenguajes de programación: sistemas de pruebas y computación cuántica. Universidad Nacional de Quilmes. 2019-2021.
3. ECOS Sud A17C01. Semantics and implementation of functional programming. 2018-2020. Extended until 2021 due to the COVID-19 crisis.
4. ECOS Sud A17C03. Quantum calculi. 2018-2020. Extended until 2021 due to the COVID-19 crisis.
5. PICT 2015-1208. Fundamentos de lenguajes de programación cuántica: hacia una lógica computacional. MinCyT. 2017-2019.
6. PUNQ 1370/17. Fundamentos de lenguajes de programación cuánticos y sus consecuencias en sistemas clásicos. Universidad Nacional de Quilmes. 2017-2019.
7. We participated in INFINIS, a French-Argentinean Laboratory (Laboratoire Internationale Associé) between Centre National de la Recherche Scientifique(CNRS) and Université Paris Diderot, on the one hand, and Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET) and the Universidad de Buenos Aires, on the other. It is devoted to research in Computer Science. Specific focus is placed on formal methods, for modeling, verification and development of complex software artifacts. 2013-2018.
8. STIC-AmSud. FoQCoSS - Foundations of Quantum Computation: Syntax and Semantics. Argentina: Universidad Nacional de Quilmes, Universidad de Buenos Aires. Brazil: Universidade Federal de Santa Maria. France: INRIA, CNRS/LORIA, Université Aix-Marseille, CentraleSupélec/LRI. 2016-2017.
9. PUNQ 1425/15. Fundamentos de lenguajes de programación cuánticos y sus consecuencias en sistemas clásicos. Universidad Nacional de Quilmes. 2015-2017.
10. PUNQ 1416/15. Programación funcional: fundamentos revisados. Universidad Nacional de Quilmes. 2015-2016.
11. ECOS Sud. Dinámica de Cálculos de Sustituciones Explícitas a Distancia.
12. STIC-AmSud. Formal Development of Computer Programs and Applications. Argentina: Universidad Nacional de Quilmes. Brazil: Universidade de Brasília. France: Laboratoire PPS, Université Paris VII. 2012-2013.
13. UBACyT 20020100100372 Diversas extensiones de sistemas de reescritura para la implementación eficiente de lenguajes de programación. Universidad de Buenos Aires. 2011-2014.
14. PUNQ 1011/11. Técnicas rigurosas para el desarrollo de software confiable. Universidad Nacional de Quilmes. 2011-2012.