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 at Universidad Nacional de Quilmes
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. I also 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: two STIC-AmSud projects, with partners also from Uruguay, Chile, and Brazil, and one ECOS-Sud project. I am also the director of the Argentinian side of the LDPL team (Logics and Dynamics of Programming Languages) at the IRP SINFIN, between CONICET and CNRS. I am also the director of the LoReL team (Logic and Rewriting for Programming Languages) between Universidad Nacional de Quilmes and Universidad de Buenos Aires, and member of the QuICC team (Quantum Information, Computation, and Communication) at the Universidad de Buenos Aires.

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

Next events

Recent past events

Current grants

Papers under review

  • A. Díaz-Caro, E. Hainry, R. Péchoux, and M. Silva. A feasible and unitary programming language with quantum control arXiv:2311.01054 - 2023 - BibTeX
  • 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. Non-determinism in a linear logic type discipline: A concrete categorical perspective. arXiv:2309.04624 - 2023 - 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 - 2022 - BibTeX

Publications

2023

  • A. Díaz-Caro and O. Malherbe. A concrete model for a typed linear algebraic lambda calculus. Mathematical Structures in Computer Science. FirstView:1-40, 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 ]

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).
  • Martín Villagra. Licenciatura thesis at UNR (DCC-FCEIA), co-supervised with P. E. Martínez López.

Past students