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
Pabellón 1, Ciudad Universitaria
C1428EGA Buenos Aires, Argentina
Office: 8
Phone: +54 11 5285-7631
Fax: +54 11 4576-3359


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
Phone: +54 11 4365-7100 # 5653



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 research position at CONICET (the Argeninian national scientific council), affiliated to the Instituto de Ciencias de la Computación at the Universidad de Buenos Aires. I also hold a tenured professorship at the Universidad Nacional de Quilmes.

I got my PhD in 2011 at the Université de Grenoble, working on type theory and quantum computing, and did postdocs at the Université Paris 13 (LIPN), Inria, and the Università di Torino.

I have directed three international research projects between Argentina and France: two STIC-AmSud projects, with partners also from Uruguay, Chile, and Brazil, and one ECOS-Sud project (see below). 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) at the Universidad Nacional de Quilmes and member of the QuICC team (Quantum Information, Computation and Communication) at the Universidad de Buenos Aires. I am member of the Steering Committee of FSCD.

Next events

Recent past events

Grants

Submitted papers and drafts

With extended abstract accepted at workshops

  • A note on confluence in typed probabilistic lambda calculi
    R. Romero and A. Díaz-Caro - arXiv:2106.06633 (Extended abstract at LSFA'21) - 2021 - BibTeX .
  • A finite-dimensional model for affine, linear quantum lambda calculi with general recursion
    A. Díaz-Caro, M. Ivnisky, H. Melgratti, and B. Valiron - PDF draft - 2021 - BibTeX (Extended abstract at TYPES'21).
  • Quantum control in the unitary sphere: Lambda-S1 and its categorical model
    A. Díaz-Caro and O. Malherbe - arXiv:2012.05887 - 2021 - BibTeX (Extended abstract at QPL'21 | Video presentation).

Other submitted papers

  • The Vectorial Lambda Calculus Revisited
    F. Noriega and A. Díaz-Caro - arXiv:2007.03648 - 2021 - BibTeX
  • A concrete model for a typed linear algebraic lambda calculus (Long revisited journal version of ENTCS 344:83-100, 2018)
    A. Díaz-Caro and O. Malherbe - arXiv:1806.09236 - 2021 - BibTeX
  • Extensional proofs in a propositional logic modulo isomorphisms
    A. Díaz-Caro and G. Dowek - arXiv:2002.03762 - 2020 - BibTeX
  • Classically Time-Controlled Quantum Automata: Definition and Properties (Long revisited journal version of LNCS 11324:266-278, 2018)
    A. Díaz-Caro and M. Villagra - arXiv:1807.05385 - 2020 - BibTeX

Publications

International peer-reviewed papers

  • A new connective in natural deduction, and its application to quantum computing
    A. Díaz-Caro and G. Dowek - (ICTAC 2021) - LNCS (accepted for publication), 2021.
    [ arXiv | 3-pages abstract at QPL'21 | Presentation at QPL'21 ]
    BibTeX
  • Polymorphic System I
    C. F. Sottile, A. Díaz-Caro, and P. E. Martínez López - (IFL 2020) - ACM Proceedings of IFL'20, pages 127-137, 2020
    [ arXiv | ACM ] doi:10.1145/3462172.3462198

    BibTeX
  • A Categorical Construction for the Computational Definition of Vector Spaces
    A. Díaz-Caro and O. Malherbe - Applied Categorical Structures 28(5):807-844, 2020
    [ arXiv | ACS | Extended abstract at ACT'19] doi:10.1007/s10485-020-09598-7
    BibTeX
  • Functional Pearl: The Distributive λ-Calculus
    B. Accattoli and A. Díaz-Caro - (FLOPS 2020) - LNCS 12073:13-32, 2020.
    [ arXiv | LNCS ] doi:10.1007/978-3-030-59025-3_3
    BibTeX
  • Extended abstract: Runtime Analysis of Quantum Programs: A Formal Approach
    F. Olmedo and A. Díaz-Caro - (PLanQC 2020) - Extended abstract, 2020.
    [ arXiv | Abstract at PLanQC ]
    BibTeX
  • Two linearities for quantum computing in the lambda calculus
    A. Díaz-Caro, G. Dowek, and J. P. Rinaldi - Postproceedings of TPNC'2017. Biosystems 186:104012, 2019.
    [ arXiv | BioSystems | Slides at CVQT'18] doi:10.1016/j.biosystems.2019.104012
    BibTeX
  • Proof Normalisation in a Logic Identifying Isomorphic Propositions
    A. Díaz-Caro and G. Dowek - (FSCD 2019) - LIPIcs 131:14, 2019.
    arXiv | LIPIcs | slides ] doi:10.4230/LIPIcs.FSCD.2019.14
    BibTeX
  • Realizability in the Unitary Sphere
    A. Díaz-Caro, M. Guillermo, A. Miquel, and B. Valiron - LICS 2019.
    [ IEEE | arXiv ] doi:10.1109/LICS.2019.8785834
    BibTeX
  • Classically time-controlled quantum automata
    A. Díaz-Caro and M. Villagra - (TPNC 2018) - LNCS 11324:266-278, 2018.
    [ arXiv | LNCS ] doi:10.1007/978-3-030-04070-3_21
    BibTeX
  • A concrete categorical semantics for Lambda-S
    A. Díaz-Caro and O. Malherbe - (LSFA 2018) - ENTCS 344:83-100, 2018.
    [ ENTCS | slides ] doi:10.1016/j.entcs.2019.07.006
    BibTeX
  • Confluence in probabilistic rewriting
    A. Díaz-Caro and G. Martínez - (LSFA 2017) - ENTCS 338:115-131, 2018.
    [ arXiv | ENTCS ] doi:10.1016/j.entcs.2018.10.008
    BibTeX
  • Typing quantum superpositions and measurement
    A. Díaz-Caro and G. Dowek - (TPNC 2017) - LNCS 10687:281-293, 2017.
    [ arXiv | LNCS | Poster (APLAS'17) | slides ] doi:10.1007/978-3-319-71069-3_22
    BibTeX
  • A lambda calculus for density matrices with classical and probabilistic controls
    A. Díaz-Caro - (APLAS 2017) - LNCS 10695:448-467, 2017.
    [ arXiv | LNCS | slides ] doi:10.1007/978-3-319-71237-6_22
    BibTeX
  • The vectorial λ-calculus
    P. Arrighi, A. Díaz-Caro, and B. Valiron - Information and computation 254(1):105-139, 2017.
    [ arXiv | IC ] doi:10.1016/j.ic.2017.04.001
    BibTeX
  • Retractions in intersection types
    M. Coppo, M. Dezani-Ciancaglini, A. Díaz-Caro, I. Margaria and M. Zacchi - (ITRS 2016) - EPTCS 242:31-47, 2017.
    [ EPTCS ] doi:10.4204/EPTCS.242.5
    BibTeX
  • Affine computation and affine automaton
    A. Díaz-Caro and A. Yakaryılmaz - (CSR 2016) - LNCS 9691:146-160, 2016.
    [ arXiv | LNCS | slides ] doi:10.1007/978-3-319-34171-2_11
    BibTeX
  • Isomorphisms considered as equalities
    Projecting functions and enhancing partial application through an implementation of λ⁺

    A. Díaz-Caro and P. E. Martínez López - (IFL 2015) - ACM Proceedings of IFL'15(9), 2015.
    [ arXiv | ACM | prototipe ] doi:10.1145/2897336.2897346
    BibTeX
  • Call-by-value, call-by-name and the vectorial behaviour of the algebraic λ-calculus
    A. Assaf, A. Díaz-Caro, S. Perdrix, C. Tasson, and B. Valiron - Logical Methods in Computer Science 10(4:8), 2014.
    [ LMCS ] doi:10.2168/LMCS-10(4:8)2014
    BibTeX
  • The probability of non-confluent systems
    A. Díaz-Caro and G. Dowek - (DCM 2013) - EPTCS 144:1-15, 2014.
    [ EPTCS | slides ] doi:10.4204/EPTCS.144.1
    BibTeX
  • Call-by-value non-determinism in a linear logic type discipline
    A. Díaz-Caro, G. Manzonetto, and M. Pagani - (LFCS 2013) - LNCS 7734:164-178, 2013.
    [ HAL | LNCS | slides ] doi:10.1007/978-3-642-35722-0_12
    BibTeX
  • Non determinism through type isomorphism
    A. Díaz-Caro and G. Dowek - (LSFA 2012) - EPTCS 113:137-144, 2013.
    [ EPTCS | slides ] doi:10.4204/EPTCS.113.13
    BibTeX
  • A System F accounting for scalars
    P. Arrighi and A. Díaz-Caro - Logical Methods in Computer Science 8(1:11), 2012
    [ LMCS | slides ] doi:10.2168/LMCS-8(1:11)2012
    BibTeX
  • Linearity in the non-deterministic call-by-value setting
    A. Díaz-Caro and B. Petit - (WoLLIC 2012) - LNCS 7456:216-231, 2012.
    [ arXiv | LNCS | slides ] doi:10.1007/978-3-642-32621-9_16
    BibTeX
  • Confluence via strong normalisation in an algebraic λ-calculus with rewriting
    P. Buiras, A. Díaz-Caro, and M. Jaskelioff - (LSFA 2011) - EPTCS 81:16-29, 2012.
    [ EPTCS | slides (QuAND) ] doi:10.4204/EPTCS.81.2
    BibTeX
  • A type system for the vectorial aspect of the linear-algebraic lambda-calculus
    P. Arrighi, A. Díaz-Caro, and B. Valiron - (DCM 2011) - EPTCS 88:1-15, 2012.
    [ EPTCS | COQ proof advertised in the paper | slides ] doi:10.4204/EPTCS.88.1
    BibTeX
  • Equivalence of algebraic λ-calculi - work-in-progress
    A. Díaz-Caro, S. Perdrix, C. Tasson, and B. Valiron - HOR 2010, Pre-proceedings, pp.6-11, Edinburgh, UK, July 14, 2010
    [ arXiv | slides | HOR 2010 site ] doi:10.13140/RG.2.1.2528.4961
    BibTeX
  • Scalar System F for linear-algebraic λ-calculus: Towards a quantum physical logic
    P. Arrighi and A. Díaz-Caro - (QPL 2009) - ENTCS 270(2):219-229, 2011.
    [ arXiv | ENTCS | slides ] doi:10.1016/j.entcs.2011.01.033
    BibTeX
  • Measurements and confluence in quantum lambda calculi with explicit qubits
    A. Díaz-Caro, P. Arrighi, M. Gadella, and J. J. Grattage - (QPL/DCM 2008) - ENTCS 270(1):59-74, 2011.
    [ arXiv | ENTCS ] doi:10.1016/j.entcs.2011.01.006
    BibTeX

Theses

  • PhD Thesis: Du typage vectoriel
    A. Díaz-Caro. Advisor: P. Arrighi. Co-advisor: F. Prost - Université de Grenoble, France, Sep. 23, 2011
    [ pdf | slides | video (only the dissertation part) | TEL ]
    BibTeX
  • Master's Thesis: Agregando medición al cálculo de van Tonder
    A. Díaz-Caro. Advisors M. Gadella and P. E. Martínez López - Universidad Nacional de Rosario, Argentina, Dec. 21, 2007
    [ pdf | slides ]
    BibTeX

Science popularisation

  • Radio interview
    Interview by the radio show "El Faro - Un programa de ciencia" (FM Radio Noticias, Santa Rosa, La Pampa).
    [ RadioCut ] October 15, 2020.
  • ¿Qué es la computación cuántica?
    A. Díaz-Caro - Ciencia Hoy 25(150):40-44, 2016
    [ Ciencia Hoy ] ISSN: 0327-1218
  • Tras las huellas de la computación cuántica
    A. Díaz-Caro - Ensemble 9: Dossier Temático "Vidas y proyectos de jóvenes científicos argentinos", 2012
    [ PDF ] ISSN: 1852-5911

2020

[UNLPam]
[UNQ]

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)

  • Ignacio Grima. Licenciatura thesis at UNR (DCC-FCEIA). Co-supervisor: P. E. Martínez López.
  • Nicolás Monzón. Licenciatura thesis at UADE.
  • Nicolás San Martín. Licenciatura thesis at UBA (DC-FCEN). Co-supervisor: P. E. Martínez López.
  • Martín Villagra. Licenciatura thesis at UNR (DCC-FCEIA). Co-supervisor: P. E. Martínez López.

Past students