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
Investigador Asistente at CONICET in the Instituto de Ciencias de la Computación (FCEN - UBA)
Profesor Adjunto at Universidad Nacional de Quilmes

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

I am part of the teams LoReL, on "Logic and Rewritting for Languages", and of QuICC on "Quantum Information, Computation, and Communication". I am also member of the LDPL team of the Laboratoire International Associé SINFIN.

07/2016 - Present "Investigador Asistente" (Tenured Researcher / Charché de Recherche) at CONICET. Since 04/2018 at the ICC (FCEN-Universidad de Buenos Aires).

01/2016 - 07/2016 Visiting researcher at Universià degli Studi di Torino in the Dipartimento di Informatica, funded by a "World Wide Style Project".

08/2014 - Present "Profesor Adjunto" (Tenured Assistant Professor / Maître de Conférences) at Universidad Nacional de Quilmes. (RAICES PRI-PIDRI).

10/2012 - 08/2014 Non-tenured teaching and research position (ATER) at Université Paris Ouest Nanterre La Défense, in the Département de Mathématique et d'Informatique and associated member of the Deducteam team at INRIA Paris-Rocquencourt.

10/2011 - 09/2012 Postdoc at Université Paris 13, the LIPN laboratory, within the LCR team.

10/2008 - 09/2011 PhD student within the CAPP team at the LIG Laboratory of the Université de Grenoble, with Pablo Arrighi as advisor and Frédéric Prost as co-advisor. The thesis defense happened on September 23, 2011. You can download my thesis “Du typage vectoriel”, as well as the slides used during the presentation, and even a video, in the publications section bellow.

12/2007 graduated in Computer Science from the Universidad Nacional de Rosario.

Next events

Grants

Submitted papers and drafts

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

Publications

International peer-reviewed papers

  • A Categorical Construction for the Computational Definition of Vector Spaces
    A. Díaz-Caro and O. Malherbe - Applied Categorical Structures, 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) - to appear in LNCS, 2020.
    [ arXiv ]
    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 (free download) | 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

  • ¿Qué es la computación cuántica?
    A. Díaz-Caro - Ciencia Hoy 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

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

2019

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

Past students