My Photo

Email:


⟨first name⟩@diaz-caro.info

Address 1:


ICC

Instituto de Ciencias de la Computación
Facultad de Ciencias Exactas y Naturales
Universidad de Buenos Aires
Cero mas Infinito, Ciudad Universitaria
C1428EGA Buenos Aires, Argentina
Office: 2108-A
Phone: +54 11 5285-9739


Address 2:


Universidad Nacional de Quilmes
Departamento de Ciencia y Tecnología
Universidad Nacional de Quilmes
Roque Sáenz Peña 352
B1876BXD Bernal, Buenos Aires, Argentina
Office: 77



Teams


LoReL

QuICC










Alejandro Díaz-Caro
Profesor Adjunto (DE) at Universidad Nacional de Quilmes
Profesor Adjunto (DP) at Universidad de Buenos Aires
Investigador Adjunto at CONICET in the Instituto de Ciencias de la Computación (FCEN - UBA)

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

I hold a tenured professorship at the Universidad Nacional de Quilmes, and a part-time professorship at the Universidad de Buenos Aires. Additionally, I hold a tenured research position at CONICET (the Argentinian National Scientific Council), affiliated with the Instituto de Ciencias de la Computación at the Universidad de Buenos Aires.

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. Furthermore, I am 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, I am the director for the LoReL team (Logic and Rewriting for Programming Languages) at the Universidad Nacional de Quilmes and the Universidad de Buenos Aires. Moreover, I am a member of the QuICC team (Quantum Information, Computation, and Communication) at the Universidad de Buenos Aires.

I am also member of the Steering Committees of FSCD and ECI.

Next events

Current grants

Papers under review

  • A. Díaz-Caro, G. Dowek, M. Ivnisky, and O. Malherbe. A linear proof language for second-order intuitionistic linear logic. arXiv:2310.08517 - 2023 - BibTeX
  • A. Díaz-Caro and O. Malherbe. A General Probabilistic Framework in IMALL: A concrete categorical perspective. arXiv:2309.04624 - 2024 - BibTeX
  • A. Díaz-Caro and G. Dowek. A linear linear lambda-calculus. (Long revisited journal version of LIPIcs 228:21, 2022). arXiv:2201.11221 - 2023 - BibTeX
  • A. Díaz-Caro and O. Malherbe. Semimodules and the (syntactically-)linear lambda calculus. arXiv:2205.02142 - 2022 - BibTeX
  • A. Díaz-Caro and M. Villagra. Classically Time-Controlled Quantum Automata: Definition and Properties. (Long revisited journal version of LNCS 11324:266-278, 2018). arXiv:1807.05385 - 2023 - BibTeX

Publications

2024

  • 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'21, 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'21) - 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

  • Radio interview
    Interview by the radio show "El Faro - Un programa de ciencia" (FM Radio Noticias, Santa Rosa, La Pampa).
    [ RadioCut ] October 15, 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 ] doi:10.13140/RG.2.1.2528.4961

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

[UBA]
  • Paradigmas 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

PhD students

Licenciatura students (equivalent to Master in the Bologna system)

  • 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