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: B218
Phone: +33 3 54 95 84 21


Team:


Mocqua





Show/Hide Contact Info

Alejandro Díaz-Caro
INRIA Advanced Research Position at Loria (Mocqua team)
Profesor Adjunto (d.s.e) at Universidad Nacional de Quilmes

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

Since October 1st, 2024, I hold an Advanced Research Position from INRIA at Loria (Laboratoire lorraine de recherche en informatique et ses applications) within the Mocqua team. I also keep a tenured professorship at the Universidad Nacional de Quilmes.

I have directed several international research projects between Argentina and France, including two STIC-AmSud projects with partners from Uruguay, Chile, and Brazil, and one ECOS-Sud project. Recently, I have obtained a MSCA Staff Exchanges project called QCOMICAL, which will run from December 2024 to November 2028, involving collaborators from Argentina, Uruguay, France, and Italy. Furthermore, I was the director of the Argentinian side of the LDPL team (Logics and Dynamics of Programming Languages) at the IRP SINFIN, a collaboration between CONICET and CNRS. Additionally, until September 2024, I was the director for the LoReL team (Logic and Rewriting for Programming Languages) at the Universidad Nacional de Quilmes and the Universidad de Buenos Aires.

I was an elected member of the Steering Committee of FSCD for the period 2021-2024, and I am a member of the Steering Committee of ECI for the period 2021-2026.

Next events

Current Grants

Drafts and papers under review

  • A. Díaz-Caro and O. Malherbe. Parallel and algebraic lambda-calculi in intuitionistic propositional logic. arXiv:2408.16102 - 2024 - BibTeX
  • A. Díaz-Caro, E. Hainry, R. Péchoux, and M. Silva. A feasible and unitary quantum programming language. arXiv:2311.01054 - 2024 - BibTeX
  • A. Díaz-Caro and O. Malherbe. The sup connective in IMALL: A categorical semantics. arXiv:2205.02142 - 2024 - BibTeX

Publications

Color codes

2024

  • A. Díaz-Caro and M. Villagra. Classically time-controlled quantum automata: Definition and properties. The Computer Journal, bxae089, 2024.
    [ BibTeX | TCJ (free access) | arXiv ] doi:10.1093/comjnl/bxae089
  • 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. 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 Ciencia | PDF ] ISSN: 0718-8005 (impresa) - 0717-8013 (en línea)
  • Several posters at QPL 2024: (see details)
  • A. Díaz-Caro, G. Dowek, and O. Malherbe. Extended abstract: From Linear logic to quantum control. (QPL 2024) - Extended abstract, 2024.
    [ BibTeX | Extended abstract ]
  • 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.
    [ BibTeX | arXiv | LNCS ] doi:10.1007/978-3-031-62687-6_2
  • A. Díaz-Caro and G. Dowek. A linear linear lambda-calculus. Mathematical Structures in Computer Science, FirstView, pp 1-35, 2024.
    [ BibTeX | arXiv | MSCS ] doi:10.1017/S0960129524000197
  • A. Díaz-Caro, E. Hainry, R. Péchoux, and M. Silva. Extended abstract: A feasible and unitary programming language with quantum control (work-in-progress) (PLanQC 2024) - Extended abstract, 2024.
    [ BibTeX | Abstract ]

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.
    [ BibTeX | arXiv | MSCS ] 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
    [ BibTeX | arXiv | TCS ] 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
    [ BibTeX | arXiv | TCS ] 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.
    [ BibTeX | LMCS | 3-pages abstract at QPL'21 | Video 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.
    [ BibTeX | arXiv | LIPIcs | Video 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.
    [ BibTeX | EPTCS | Video 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.
    [ BibTeX | EPTCS | Video 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.
    [ BibTeX | arXiv | LNCS | 3-pages abstract at QPL'21 | Video at ICTAC'21 | Video 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.
    [ BibTeX | PDF ]

2020

  • 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. Disclaimer
    [ BibTeX | arXiv | ACM ] doi:10.1145/3462172.3462198
  • 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
    [ BibTeX | arXiv | ACS | Extended abstract at ACT'19] doi:10.1007/s10485-020-09598-7
  • B. Accattoli and A. Díaz-Caro. Functional Pearl: The Distributive λ-Calculus. (FLOPS 2020) - LNCS 12073:13-32, 2020.
    [ BibTeX | arXiv | LNCS ] doi:10.1007/978-3-030-59025-3_3
  • F. Olmedo and A. Díaz-Caro. Extended abstract: Runtime Analysis of Quantum Programs: A Formal Approach. (PLanQC 2020) - Extended abstract, 2020.
    [ BibTeX | arXiv | Abstract at PLanQC ]

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.
    [ BibTeX | arXiv | BioSystems | Slides 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.
    [ BibTeXarXiv | LIPIcs | slides ] 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.
    [ BibTeX | IEEE | arXiv ] 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.
    [ BibTeX | arXiv | LNCS ] 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.
    [ BibTeX | ENTCS | slides ] doi:10.1016/j.entcs.2019.07.006

2017

  • A. Díaz-Caro and G. Martínez. Confluence in probabilistic rewriting. (LSFA 2017) - ENTCS 338:115-131, 2018.
    [ BibTeX | arXiv | ENTCS ] 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.
    [ BibTeX | arXiv | LNCS | Poster (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.
    [ BibTeX | arXiv | LNCS | slides ] doi:10.1007/978-3-319-71237-6_22
  • P. Arrighi, A. Díaz-Caro, and B. Valiron. The vectorial λ-calculus. Information and computation 254(1):105-139, 2017.
    [ BibTeX | arXiv | IC ] doi:10.1016/j.ic.2017.04.001

2016

  • A. Díaz-Caro. ¿Qué es la computación cuántica?. Ciencia Hoy 25(150):40-44, 2016
    [ Ciencia Hoy ] ISSN: 0327-1218
  • 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.
    [ BibTeX | EPTCS ] 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.
    [ BibTeX | arXiv | LNCS | slides ] doi:10.1007/978-3-319-34171-2_11

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.
    [ BibTeX | arXiv | ACM | prototipe ] 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.
    [ BibTeX | LMCS ] 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.
    [ BibTeX | EPTCS | slides ] 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.
    [ BibTeX | HAL | LNCS | slides ] doi:10.1007/978-3-642-35722-0_12

2012

  • 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
  • A. Díaz-Caro and G. Dowek. Non determinism through type isomorphism. (LSFA 2012) - EPTCS 113:137-144, 2013.
    [ BibTeX | EPTCS | slides ] doi:10.4204/EPTCS.113.13
  • P. Arrighi and A. Díaz-Caro. A System F accounting for scalars. Logical Methods in Computer Science 8(1:11), 2012
    [ BibTeX | LMCS | slides ] doi:10.2168/LMCS-8(1:11)2012
  • A. Díaz-Caro and B. Petit. Linearity in the non-deterministic call-by-value setting. (WoLLIC 2012) - LNCS 7456:216-231, 2012.
    [ BibTeX | arXiv | LNCS | slides ] doi:10.1007/978-3-642-32621-9_16

2011

  • A. Díaz-Caro. Du typage vectoriel. PhD Thesis. Advisor: P. Arrighi. Co-advisor: F. Prost - Université de Grenoble, France, Sep. 23, 2011
    [ BibTeX | pdf | slides | Video | TEL ]
  • 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.
    [ BibTeX | EPTCS | slides (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.
    [ BibTeX | EPTCS | COQ proof advertised in the paper | slides ] doi:10.4204/EPTCS.88.1

2010

  • A. Díaz-Caro, S. Perdrix, C. Tasson, and B. Valiron. Equivalence of algebraic λ-calculi - work-in-progress. HOR 2010, Pre-proceedings, pp.6-11, Edinburgh, UK, July 14, 2010
    [ BibTeX | arXiv | slides ]

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.
    [ BibTeX | arXiv | ENTCS | slides ] doi:10.1016/j.entcs.2011.01.033

2007-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.
    [ BibTeX | arXiv | ENTCS ] doi:10.1016/j.entcs.2011.01.006
  • 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
    [ BibTeX | pdf | slides ]

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]
[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

Students

PhD students

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

  • Luciano Barletta. Licenciatura thesis at UNR (DCC-FCEIA).
  • Francisco Herrero. Licenciatura student at UBA (DC-FCEN), with Malena Ivnisky
  • Tomás Miguez. Licenciatura thesis at UBA (DC-FCEN).
  • Nicolás Monzón. Licenciatura thesis at UADE.
  • Álvaro Piorno. Licenciatura thesis at UNQ.
  • Carlos Miguel Soto. Licenciatura thesis at UBA (DC-FCEN).

Past students

Media Appearances and Interviews