My Photo

Email:


⟨first name⟩@diaz-caro.info

Address:


Loria
Loria

LORIA, Campus Scientifique,
615 rue du Jardin Botanique,
F54506 Vandœuvre-lès-Nancy, France
Office: B220
Phone: +33 3 83 59 20 12


Team:


Mocqua





Show/Hide Contact Info

Alejandro Díaz-Caro
INRIA — Mocqua team, LORIA, France
Universidad Nacional de Quilmes, Argentina
Universidad de la República, CENUR Suroeste, Uruguay

Visiting Researcher at INRIA
Full Professor at Universidad Nacional de Quilmes
Professor (Grado 4) at Universidad de la República (starting 2026)

Keywords: Type theory, Rewriting systems, Logic, Quantum computing

I am a Full Professor at the Universidad Nacional de Quilmes (Argentina) and a permanent Researcher at CONICET (currently on leave). Since October 2024, I have been visiting INRIA Nancy for a three-year period, hosted by the Mocqua team at Loria, as part of the PEPR integrated project EPiQ (ANR-22-PETQ-0007), funded under the France 2030 Plan. Starting in 2026, I also hold a Professor (Grado 4) position at the Universidad de la República (Uruguay), at CENUR Suroeste in Colonia del Sacramento.

I have led several international research projects between Latin America and Europe, including two STIC-AmSud projects, one ECOS-Sud project, and I co-lead the MSCA Staff Exchanges project QCOMICAL (2024–2028), involving partners from Argentina, Uruguay, France, and Italy.

I was the Argentinian director and I am currently the French director of the LDPL team (Logics and Dynamics of Programming Languages) at the IRP SINFIN, a collaboration between CONICET and CNRS. Until September 2024, I also led the LoReL team (Logic and Rewriting for Programming Languages) at the Universidad Nacional de Quilmes and Universidad de Buenos Aires. In addition, I was a member of the QuICC team (Quantum Information, Computation, and Communication) at the Universidad de Buenos Aires.

I was an elected member of the Steering Committee of FSCD from 2021 to 2024.

Current Responsibilities:

Next events


Current Grants

Drafts and papers under review

  • A. Díaz-Caro, O. Malherbe, and R. Romero. Basis-Sensitive Quantum Typing via Realisability. BibTeXarXiv
  • M. Avanzini, A. Díaz-Caro, E. Hainry, and R. Péchoux. Expectation-based Analysis of Higher-Order Quantum Programs. BibTeXarXiv
  • A. Díaz-Caro and G. Dowek. A new introduction rule for disjunction. BibTeXarXiv
  • A. Díaz-Caro, E. Hainry, R. Péchoux, and M. Silva. A feasible and unitary quantum programming language. BibTeXarXiv

Publications

2026

    • A. Díaz-Caro and O. Malherbe. The sup connective in IMALL: A categorical semantics. Theoretical Computer Science (to appear), 2026. BibTeXarXiv

2025

    • A. Díaz-Caro, M. Ivnisky, and O. Malherbe. An Algebraic Extension of Intuitionistic Linear Logic: The LS!-Calculus and Its Categorical Model. Journal of Logic and Computation 35(8):exaf053, 2025. BibTeXJLCarXiv doi:10.1093/logcom/exaf053
    • A. Díaz-Caro and M. Villagra. Classically time-controlled quantum automata: Definition and properties. The Computer Journal 68(1):23-31, 2025. BibTeXTCJ (free access)arXiv doi:10.1093/comjnl/bxae089
    • A. Díaz-Caro and O. Malherbe. Beyond Monads and Biproducts: A Uniform Interpretation of Parallelism in Intuitionistic Logic. (FSTTCS 2025) - LIPIcs 360:28, 1-17, 2025. BibTeXarXivLIPIcs doi:10.4230/LIPIcs.FSTTCS.2025.28
    • A. Díaz-Caro and N. A. Monzon. A Quantum-Control Lambda-Calculus with Multiple Measurement Bases. (APLAS 2025) - LNCS 16201:151-170, 2025. BibTeXarXivLNCS doi:10.1007/978-981-95-3585-9_8
    • K. Dave, A. Díaz-Caro, and V. Zamdzhiev. IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation. (APLAS 2025) - LNCS 16201:131-150, 2025. BibTeXarXivLNCS doi:10.1007/978-981-95-3585-9_7
    • A. Díaz-Caro. Towards a Computational Quantum Logic: An Overview of an Ongoing Research Program. (CiE 2025, invited paper) - LNCS 15764:34-46, 2025. BibTeXarXivLNCSVideo (TYPES'25) doi:10.1007/978-3-031-95908-0_3
    • C. F. Sottile and A. Díaz-Caro. Reducibility candidates modulo isomorphisms. (IFL 2025) - Extended abstract, 2025.
    • A. Díaz-Caro, G. Dowek, and J.-P. Jouannaud. Proving Termination With CPOs. (HOR 2025) - Extended abstract, 2025. HAL
    • A. Díaz-Caro, O. Malherbe, and R. Romero. Basis-Sensitive Quantum Typing via Realizability. (HOR 2025) - Extended abstract, 2025.

2024

    • A. Díaz-Caro and G. Dowek. A linear linear lambda-calculus. Mathematical Structures in Computer Science, 34(10):1103-1137, 2024. BibTeXarXivMSCS doi:10.1017/S0960129524000197
    • A. Díaz-Caro, G. Dowek, M. Ivnisky, and O. Malherbe. A linear proof language for second-order intuitionistic linear logic. (WoLLIC 2024) - LNCS 14672:18-35, 2024. BibTeXarXivLNCS doi:10.1007/978-3-031-62687-6_2
    • A. Díaz-Caro. Lógica y computación cuántica: Un camino a través de los vaivenes políticos de la Argentina. Bits de Ciencia 26:20-25, 2024 Bits de CienciaPDF ISSN: 0718-8005 (impresa) - 0717-8013 (en línea)
    • Proceedings of the 21st International Conference on Quantum Physics and Logic. Edited by A. Díaz-Caro and V. Zamdzhiev. Electronic Proceedings in Theoretical Computer Science 406, 2024. EPTCS doi:10.4204/EPTCS.406
    • A. Díaz-Caro, G. Dowek, and O. Malherbe. From Linear logic to quantum control. (QPL 2024) - Extended abstract, 2024. PDF.
    • A. Díaz-Caro, E. Hainry, R. Péchoux, and M. Silva. A feasible and unitary programming language with quantum control (work-in-progress) (PLanQC 2024) - Extended abstract, 2024. Link

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-44, 2023. BibTeXarXivMSCS doi:10.1017/s0960129523000361
    • A. Díaz-Caro and G. Dowek. Extensional proofs in a propositional logic modulo isomorphisms. Theoretical Computer Science 977:114172, 2023. BibTeXarXivTCS doi:10.1016/j.tcs.2023.114172
    • 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. BibTeXarXivTCS doi:10.1016/j.tcs.2023.113840

2022

    • A. Díaz-Caro and O. Malherbe. Quantum control in the unitary sphere: Lambda-S1 and its categorical model. Logical Methods in Computer Science 18(3:32), 2022. BibTeXLMCS3-pages abstract at QPL'21Video at QPL'21 doi:10.46298/lmcs-18(3:32)2022
    • A. Díaz-Caro and G. Dowek. Linear Lambda-Calculus is Linear. (FSCD 2022) - LIPIcs 228:21, 2022. BibTeXarXivLIPIcsVideo at FSCD'22 doi:10.4230/LIPIcs.FSCD.2022.21

2021

    • A. Díaz-Caro. A quick overview on the quantum control approach to the lambda calculus. (LSFA 2021, invited paper) - EPTCS 357:1-17, 2021. BibTeXEPTCSVideo at LSFA'21 doi:10.4204/EPTCS.357.1
    • R. Romero and A. Díaz-Caro. A note on confluence in typed probabilistic lambda calculi. (LSFA 2021) - EPTCS 357:18-24, 2021. BibTeXEPTCSVideo at LSFA'21 doi:10.4204/EPTCS.357.2
    • A. Díaz-Caro and G. Dowek. A new connective in natural deduction, and its application to quantum computing. (ICTAC 2021) - Best Paper Award - LNCS 12819:175-193, 2021. BibTeXarXivLNCS3-pages abstract at QPL'21Video at ICTAC'21Video at QPL'21 doi:10.1007/978-3-030-85315-0_11
    • A. Díaz-Caro, M. Ivnisky, H. Melgratti, and B. Valiron. A finite-dimensional model for affine, linear quantum lambda calculi with general recursion. (TYPES 2021) - Extended abstract, 2021. Link

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. BibTeXarXivACSExtended abstract at ACT'19 doi:10.1007/s10485-020-09598-7
    • C. F. Sottile, A. Díaz-Caro, and P. E. Martínez López. Polymorphic System I. (IFL 2020) - ACM Proceedings of IFL'20, pages 127-137, 2020. Erratum BibTeXarXivACM doi:10.1145/3462172.3462198
    • B. Accattoli and A. Díaz-Caro. Functional Pearl: The Distributive λ-Calculus. (FLOPS 2020) - LNCS 12073:13-32, 2020. BibTeXarXivLNCS doi:10.1007/978-3-030-59025-3_3
    • F. Olmedo and A. Díaz-Caro. Runtime Analysis of Quantum Programs: A Formal Approach. (PLanQC 2020) - Extended abstract, 2020. arXiv

2019

    • A. Díaz-Caro, G. Dowek, and J. P. Rinaldi. Two linearities for quantum computing in the lambda calculus. Postproceedings of TPNC'2017. Biosystems 186:104012, 2019. BibTeXarXivBioSystemsSlides at CVQT'18 doi:10.1016/j.biosystems.2019.104012
    • A. Díaz-Caro and G. Dowek. Proof Normalisation in a Logic Identifying Isomorphic Propositions. (FSCD 2019) - LIPIcs 131:14, 2019. BibTeXarXivLIPIcsslides doi:10.4230/LIPIcs.FSCD.2019.14
    • A. Díaz-Caro, M. Guillermo, A. Miquel, and B. Valiron. Realizability in the Unitary Sphere. LICS 2019. BibTeXIEEEarXiv doi:10.1109/LICS.2019.8785834

2018

    • A. Díaz-Caro and M. Villagra. Classically time-controlled quantum automata. (TPNC 2018) - LNCS 11324:266-278, 2018. BibTeXarXivLNCS doi:10.1007/978-3-030-04070-3_21
    • A. Díaz-Caro and O. Malherbe. A concrete categorical semantics for Lambda-S. (LSFA 2018) - ENTCS 344:83-100, 2018. BibTeXENTCSslides doi:10.1016/j.entcs.2019.07.006

2017

    • P. Arrighi, A. Díaz-Caro, and B. Valiron. The vectorial λ-calculus. Information and computation 254(1):105-139, 2017. BibTeXarXivIC doi:10.1016/j.ic.2017.04.001
    • A. Díaz-Caro and G. Martínez. Confluence in probabilistic rewriting. (LSFA 2017) - ENTCS 338:115-131, 2018. BibTeXarXivENTCS doi:10.1016/j.entcs.2018.10.008
    • A. Díaz-Caro and G. Dowek. Typing quantum superpositions and measurement. (TPNC 2017) - LNCS 10687:281-293, 2017. BibTeXarXivLNCSPoster (APLAS'17) | slides doi:10.1007/978-3-319-71069-3_22
    • A. Díaz-Caro. A lambda calculus for density matrices with classical and probabilistic controls. (APLAS 2017) - LNCS 10695:448-467, 2017. BibTeXarXivLNCSslides doi:10.1007/978-3-319-71237-6_22

2016

    • M. Coppo, M. Dezani-Ciancaglini, A. Díaz-Caro, I. Margaria and M. Zacchi. Retractions in intersection types. (ITRS 2016) - EPTCS 242:31-47, 2017. BibTeXEPTCS doi:10.4204/EPTCS.242.5
    • A. Díaz-Caro and A. Yakaryılmaz. Affine computation and affine automaton. (CSR 2016) - LNCS 9691:146-160, 2016. BibTeXarXivLNCSslides doi:10.1007/978-3-319-34171-2_11
    • A. Díaz-Caro. ¿Qué es la computación cuántica?. Ciencia Hoy 25(150):40-44, 2016. Ciencia Hoy ISSN: 0327-1218

2015

    • 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 λ⁺. (IFL 2015) - ACM Proceedings of IFL'15(9), 2015. BibTeXarXivACMPrototipe doi:10.1145/2897336.2897346

2014

    • 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. BibTeXLMCS doi:10.2168/LMCS-10(4:8)2014

2013

    • A. Díaz-Caro and G. Dowek. The probability of non-confluent systems. (DCM 2013) - EPTCS 144:1-15, 2014. BibTeXEPTCSslides doi:10.4204/EPTCS.144.1
    • A. Díaz-Caro, G. Manzonetto, and M. Pagani. Call-by-value non-determinism in a linear logic type discipline. (LFCS 2013) - LNCS 7734:164-178, 2013. BibTeXHALLNCSslides doi:10.1007/978-3-642-35722-0_12

2012

    • P. Arrighi and A. Díaz-Caro. A System F accounting for scalars. Logical Methods in Computer Science 8(1:11), 2012. BibTeXLMCSslides doi:10.2168/LMCS-8(1:11)2012
    • A. Díaz-Caro and G. Dowek. Non determinism through type isomorphism. (LSFA 2012) - EPTCS 113:137-144, 2013. BibTeXEPTCSslides doi:10.4204/EPTCS.113.13
    • A. Díaz-Caro and B. Petit. Linearity in the non-deterministic call-by-value setting. (WoLLIC 2012) - LNCS 7456:216-231, 2012. BibTeXarXivLNCSslides doi:10.1007/978-3-642-32621-9_16
    • A. Díaz-Caro. Tras las huellas de la computación cuántica. Ensemble 9: Dossier Temático "Vidas y proyectos de jóvenes científicos argentinos", 2012. PDF ISSN: 1852-5911

2011

    • A. Díaz-Caro. Du typage vectoriel. PhD Thesis. Advisor: P. Arrighi. Co-advisor: F. Prost - Université de Grenoble, France, Sep. 23, 2011. BibTeXpdfslidesVideoTEL
    • P. Buiras, A. Díaz-Caro, and M. Jaskelioff. Confluence via strong normalisation in an algebraic λ-calculus with rewriting. (LSFA 2011) - EPTCS 81:16-29, 2012. BibTeXEPTCSslides (QuAND) doi:10.4204/EPTCS.81.2
    • P. Arrighi, A. Díaz-Caro, and B. Valiron. A type system for the vectorial aspect of the linear-algebraic lambda-calculus. (DCM 2011) - EPTCS 88:1-15, 2012. BibTeXEPTCSCOQ proof advertised in the paperslides doi:10.4204/EPTCS.88.1

2010

2009

    • P. Arrighi and A. Díaz-Caro. Scalar System F for linear-algebraic λ-calculus: Towards a quantum physical logic. (QPL 2009) - ENTCS 270(2):219-229, 2011. BibTeXarXivENTCSslides doi:10.1016/j.entcs.2011.01.033

2008

    • A. Díaz-Caro, P. Arrighi, M. Gadella, and J. J. Grattage. Measurements and confluence in quantum lambda calculi with explicit qubits. (QPL/DCM 2008) - ENTCS 270(1):59-74, 2011. BibTeXarXivENTCS doi:10.1016/j.entcs.2011.01.006

2007

    • A. Díaz-Caro. Agregando medición al cálculo de van Tonder. Master's Thesis. Advisors M. Gadella and P. E. Martínez López - Universidad Nacional de Rosario, Argentina, Dec. 21, 2007. BibTeXpdfslides

Media Appearances and Interviews


2026

[FING]
  • Lógica - Ingeniería en Informatica.

2025

[UBA]
[UNQ]
  • Características de Lenguajes de Programación - Licenciatura en Informática.
  • Lógica y Programación - Licenciatura en Informática.

2024

[UNQ]
[UBA]
  • Paradigmas de (Lenguajes de) Programación - Licenciatura en Ciencias de la Computación.

2023

[UNQ]
  • Características de Lenguajes de Programación - Licenciatura en Informática.
  • Lógica y Programación - Licenciatura en Informática (both semesters).
  • Probabilidad y Estadística aplicada a la Bioinformática - Maestría en Bioinformática y Biología de Sistemas.

2022

[UBA]
  • Fundamentos de Lenguajes para Computación Cuántica - Licenciatura y Doctorado en Ciencias de la Computación.
[UNQ]
  • Características de Lenguajes de Programación - Licenciatura en Informática.

2021

[UNQ]
  • Características de Lenguajes de Programación - Licenciatura en Informática.
  • Introducción a la Programación Cuántica - Licenciatura en Informática.
[UNNOBA]
  • Probabilidad y Estadística aplicada a la Bioinformática - Maestría en Bioinformática y Biología de Sistemas.

2020

[UNLPam]
[UNQ]
  • Características de Lenguajes de Programación - Licenciatura en Informática.
  • Lógica y Programación - Licenciatura en Informática.
  • Probabilidad y Estadística aplicada a la Bioinformática - Maestría en Bioinformática y Biología de Sistemas.
  • Fundamentos de informática - Doctorado en Ciencia y Tecnología.

2019

[UNQ]
  • Características de Lenguajes de Programación - Licenciatura en Informática.
  • Lenguajes Formales y Autómatas - Licenciatura en Informática.
  • Matemática II - Tecnicatura en Programación Informática (en Capitán Sarmiento, Prov. de Buenos Aires).
[UnB]

2018

[UNNOBA]
  • Probabilidad y Estadística aplicada a la Bioinformática - Maestría en Bioinformática y Biología de Sistemas.
[UNQ]
  • Características de Lenguajes de Programación - Licenciatura en Informática.
  • Matemática II - Licenciatura en Informática.
[UNR]

2017

[UNQ]
  • Características de Lenguajes de Programación - Licenciatura en Informática.
  • Matemática III - Licenciatura en Informática.
  • Matemática II - Licenciatura en Informática.
  • Probabilidad y Estadística aplicada a la Bioinformática - Maestría en Bioinformática y Biología de Sistemas.
[UBA]

2016

[UNR]
  • Introducción a la Computación Cuántica y Fundamentos de Lenguajes de Programación - Lic. en Ciencias de la Computación (materia optativa) con créditos para el doctorado.
[UNQ]
  • Características de Lenguajes de Programación - Licenciatura en Informática.
  • Matemática III - Licenciatura en Informática.
  • Matemática II - Licenciatura en Informática.
[UNSL]
  • Fundamentos de Lenguajes de Programación para Computación Cuántica - Curso de 25hs en la Escuela de Informática del CACIC.

2015

[UNQ]
  • Características de Lenguajes de Programación - Licenciatura en Informática.
  • Matemática III - Licenciatura en Informática.
  • Matemática II - Licenciatura en Informática.
  • Lenguajes Formales y Autómatas - Licenciatura en Informática.
  • Probabilidad y Estadística aplicada a la Bioinformática - Maestría en Bioinformática y Biología de Sistemas.
[UNRC]

2014

[UNNOBA]
  • Probabilidad y Estadística aplicada a la Bioinformática - Maestría en Bioinformática y Biología de Sistemas.
[UNQ]
  • Características de Lenguajes de Programación - Licenciatura en Informática.

2013-2014

[UPOND]
  • Probabilités - TD - L2 Économie et gestion.
  • Statistiques et probabilités - TD - L2 Économie et droit.
  • Méthodologie de la mesure en sciences humaines - TD - L1 Psychologie.
  • Mathématiques 2 - TD - L1 Économie et gestion.
  • Mathématiques 1: Calcul et fonctions - TD - L1 Économie et droit.

2012-2013

[UPOND]
  • Statistiques et probabilités - TD - L2 Économie et droit.
  • Méthodologie de la mesure en sciences humaines - TD - L1 Psychologie.
  • Mathématiques 2 - TD - L1 Économie et gestion.
  • Mathématiques 1: Calcul et fonctions - TD - L1 Économie et droit.
  • Mathématiques 1 - TD - L1 Économie et gestion.

2010

[ESISAR]
[UJF]
  • INF122B: Compléments mathématiques et introduction à la logique et la preuve formelle - TD - L1 Informatique.

2009

[ESISAR]
  • MA512: Théorie des graphes - TD+CM - Cycle Ingénieur - 5e année - Électronique, Informatique, Systèmes.

2008

[UNR]
  • Algebra y Geometría Analítica I - Ayudante de 1ra - Escuela de Formación Básica.
  • Análisis Matemático I - Ayudante de 1ra - Escuela de Formación Básica.

2007

[UNR]
  • Análisis Matemático IV - Ayudante de 2da - Departamento de Ciencias de la Computación.

Current students

PhD students

Licenciatura students (equivalent to Master 2 in the Bologna system)

  • Juan Bautista Figueredo. Licenciatura thesis at UNR (DCC-FCEIA). Co-director: K. Chardonnet.

Past students