Contact information:
Email:
alejan...@diazcaro.info
(GPG key)
Address:
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 43657100 # 5653

Alejandro DíazCaro
Profesor Adjunto (D.E.)
Departamento de Ciencia y Tecnología
Universidad Nacional de Quilmes
Keywords: Type theory, Rewriting systems, Logic, Quantum computing
Since August 2014 I am "Profesor Adjunto de Dedicación Exclusiva" (Tenured Assistant Professor / Maître de Conférences) at Universidad Nacional de Quilmes, in the Departamento de Ciencia y Tecnología. I am part of the LoReL team, and also integrate the Logics and Dynamics of Programming Languages team of the Laboratoire International Associé INFINIS.
From October 2012 to August 2014 I had a nontenured 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 ParisRocquencourt.
Before that, I did a postdoc from October 2011 to September 2012 at Université Paris 13, the LIPN laboratory, within the LCR team.
Even before that, between October 2008 and September 2011 I prepared my thesis within the CAPP team at the LIG Laboratory of the Université de Grenoble, with Pablo Arrighi as advisor and Frédéric Prost as coadvisor. You can download my thesis “Du typage vectoriel” in the publications section bellow.
In the prehistory I graduated in Computer Science from the Universidad Nacional de Rosario, Argentina in December 2007
Manuscripts

The vectorial lambdacalculus
(hide)
P. Arrighi, A. DíazCaro, and B. Valiron
 arXiv:1308.1138
[ arXiv ]
We describe a type system for the linearalgebraic
lambdacalculus. The type system accounts for the linearalgebraic aspects of this extension of lambdacalculus: It is
able to statically describe the linear combinations of terms
that will be obtained when reducing the programs. This gives rise to an
original type theory where types, in the same way as terms, can be
superposed into linear combinations.
We prove that the resulting
typed lambdacalculus is strongly normalising and features a weak subject reduction. Finally,
we show how to naturally encode matrices and vectors in this typed calculus.
@Misc{ArrighiDiazcaroValiron13,
author = "Pablo Arrighi and Alejandro D{\'\i}azCaro and Beno\^it Valiron",
title = "The Vectorial LambdaCalculus",
year = "2013",
note = "Submitted",
howpublished = "{\tt arXiv:1308.1138}"
}
Publications

Simply typed lambdacalculus modulo type isomorphisms
(hide)
A. DíazCaro and G. Dowek
 Considered for publication in TCS, 2015.
[ HAL (Draft. Minor revisions to be made)  Slides at TYPES'14 ]
doi:notyet
We define a simply typed, nondeterministic lambdacalculus where isomorphic types are equated. To this end, an equivalence relation is settled at the term level. We then provide a proof of strong normalisation modulo equivalence. Such a proof is a nontrivial adaptation of the reducibility method.
@Misc{DiazcaroDowekTCS15,
author = "Alejandro D{\'\i}azCaro and Gilles Dowek",
title = "Simply typed lambdacalculus modulo type isomorphisms",
year = "2015",
note = "Considered for publication in TCS",
howpublished = "Draft at https://hal.inria.fr/hal01109104"
}

Callbyvalue, callbyname and the vectorial behaviour of the algebraic λcalculus
(hide)
A. Assaf, A. DíazCaro, S. Perdrix, C. Tasson, and B. Valiron
 Logical Methods in Computer Science 10(4:8), 2014.
[ LMCS ]
doi:10.2168/LMCS10(4:8)2014
We examine the relationship between the algebraic λcalculus, a fragment of the differential λcalculus and the linearalgebraic λcalculus, a candidate λcalculus for quantum computation. Both calculi are algebraic: each one is equipped with an additive and a scalarmultiplicative structure, and their set of terms is closed under linear combinations. However, the two languages were built using different approaches: the former is a callbyname language whereas the latter is callbyvalue; the former considers algebraic equalities whereas the latter approaches them through rewrite rules.
In this paper, we analyse how these different approaches relate to one another. To this end, we propose four canonical languages based on each of the possible choices: callbyname versus callbyvalue, algebraic equality versus algebraic rewriting. We show that the various languages simulate one another. Due to subtle interaction between betareduction and algebraic rewriting, to make the languages consistent some additional hypotheses such as confluence or normalisation might be required. We carefully devise the required properties for each proof, making them general enough to be valid for any sublanguage satisfying the corresponding properties.
@Article{AssafDiazcaroPerdrixTassonValironLMCS14,
author = "Ali Assaf and Alejandro D{\'\i}azCaro and Simon Perdrix and Christine Tasson and Beno{\^\i}t Valiron",
title = "Callbyvalue, callbyname and the vectorial behaviour of the algebraic $\lambda$calculus",
journal = "Logical Methods in Computer Science",
volume = "10",
number = "4:8",
year = "2014"
}

The probability of nonconfluent systems
(hide)
A. DíazCaro and G. Dowek
 (DCM 2013)  EPTCS 144:115, 2014.
[ EPTCS  slides ]
doi:10.4204/EPTCS.144.1
We show how to provide a structure of probability space to the set of execution traces on a nonconfluent abstract rewrite system, by defining a variant of a Lebesgue measure on the space of traces. Then, we show how to use this probability space to transform a nondeterministic calculus into a probabilistic one. We use as example λ_{+}, a recently introduced calculus defined with techniques from deduction modulo.
@InProceedings{DiazcaroDowekDCM13,
author = "Alejandro D{\'\i}azCaro and Gilles Dowek",
title = "The probability of nonconfluent systems",
pages = "115",
year = "2014",
editor = "Mauricio AyalaRincón and Eduardo Bonelli and Ian Mackie",
booktitle = "Proceedings of the 9th International Workshop on Developments in Computational Models",
series = "Electronic Proceedings in Theoretical Computer Science",
volume = "144",
publisher = "Open Publishing Association"
}

Callbyvalue nondeterminism in a linear logic type discipline
(hide)
A. DíazCaro, G. Manzonetto, and M. Pagani
 (LFCS 2013)  LNCS 7734:164178, 2013.
[ HAL  LNCS  slides ]
doi:10.1007/9783642357220_12
We consider the callbyvalue λcalculus extended with a mayconvergent nondeterministic choice and a mustconvergent parallel composition. Inspired by recent works on the relational semantics of linear logic and nonidempotent intersection types, we endow this calculus with a type system based on the socalled Girard's second translation of intuitionistic logic into linear logic. We prove that a term is typable if and only if is converging, and that its typing tree carries enough information to give a bound on the length of its lazy callbyvalue reduction. Moreover, when the typing tree is minimal, such a bound becomes the exact length of the reduction.
@InProceedings{DiazcaroManzonettoPaganiLFCS13,
author = "Alejandro D{\'\i}azCaro and Giulio Manzonetto and Michele Pagani",
title = "Callbyvalue nondeterminism in a linear logic type discipline",
booktitle = "Logical Foundations of Computer Science, International Symposium, (LFCS 2013)",
editor = "Sergei Artemov and Anil Nerode",
series = "Lecture Notes in Computer Science",
publisher = "Springer Berlin Heidelberg",
pages = "164178",
volume = "7734",
year = "2013"
}

Non determinism through type isomorphism
(hide)
A. DíazCaro and G. Dowek
 (LSFA 2012)  EPTCS 113:137144, 2013.
[ EPTCS  slides ]
doi:10.4204/EPTCS.113.13
We define an equivalence relation on propositions and a proof system where equivalent propositions have the same proofs. The system obtained this way resembles several known nondeterministic and algebraic lambdacalculi.
@InProceedings{DiazcaroDowekLSFA12,
author = "Alejandro D{\'\i}azCaro and Gilles Dowek",
title = "Non determinism through type isomorphism",
pages = "137144",
year = "2013",
editor = "Delia Kesner and Petrucio Viana",
booktitle = "Proceedings of the 7th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2012)",
series = "Electronic Proceedings in Theoretical Computer Science",
volume = "113",
publisher = "Open Publishing Association"
}

Linearity in the nondeterministic callbyvalue setting
(hide)
A. DíazCaro and B. Petit
 (WoLLIC 2012)  LNCS 7456:216231, 2012.
[ arXiv  LNCS  slides ]
doi:10.1007/9783642326219_16
We consider the nondeterministic extension of the callbyvalue lambda calculus, which corresponds to the additive fragment of the linearalgebraic lambdacalculus. We define a finegrained type system, capturing the right linearity present in such formalisms. After proving the subject reduction and the strong normalisation properties, we propose a translation of this calculus into the System F with pairs, which corresponds to a non linear fragment of linear logic. The translation provides a deeper understanding of the linearity in our setting.
@InProceedings{DiazcaroPetitWoLLIC12,
author = "Alejandro D{\'\i}azCaro and Barbara Petit",
title = "Linearity in the nondeterministic callbyvalue setting",
booktitle = "Logic, Language, Information and Computation",
editor = "Luke Ong and Ruy {de Queiroz}",
series = "Lecture Notes in Computer Science",
publisher = "Springer Berlin Heidelberg",
pages = "216231",
volume = "7456",
year = "2012"
}

A System F accounting for scalars
(hide)
P. Arrighi and A. DíazCaro
 Logical Methods in Computer Science 8(1:11), 2012
[ LMCS  slides ]
doi:10.2168/LMCS8(1:11)2012
The Algebraic lambdacalculus and the LinearAlgebraic lambdacalculus extend the lambdacalculus with the possibility of making arbitrary linear combinations of terms. In this paper we provide a finegrained, System Flike type system for the linearalgebraic lambdacalculus. We show that this Scalar type system enjoys both the subjectreduction property and the strongnormalisation property, our main technical results. The latter yields a significant simplification of the linearalgebraic lambdacalculus itself, by removing the need for some restrictions in its reduction rules. But the more important, original feature of this scalar type system is that it keeps track of 'the amount of a type' that is present in each term. As an example of its use, we shown that it can serve as a guarantee that the normal form of a term is barycentric, i.e. that its scalars are summing to one.
@Article{ArrighiDiazcaroLMCS12,
author = "Pablo Arrighi and Alejandro D{\'\i}azCaro",
title = "A {S}ystem {F} accounting for scalars",
journal = "Logical Methods in Computer Science",
volume = "8",
number = "1:11",
year = "2012"
}

Confluence via strong normalisation in an algebraic λcalculus with rewriting
(hide)
P. Buiras, A. DíazCaro, and M. Jaskelioff
 (LSFA 2011)  EPTCS 81:1629, 2012.
[ EPTCS  slides (QuAND) ]
doi:10.4204/EPTCS.81.2
The linearalgebraic λcalculus and the algebraic λcalculus are untyped λcalculi extended with arbitrary linear combinations of terms. The former presents the axioms of linear algebra in the form of a rewrite system, while the latter uses equalities. When given by rewrites, algebraic λcalculi are not conﬂuent unless further restrictions are added. We provide a type system for the linearalgebraic λcalculus enforcing strong normalisation, which gives back conﬂuence. The type system allows an interpretation in System F.
@InProceedings{BuirasDiazcaroJaskelioffLSFA11,
author = "Pablo Buiras and Alejandro D{\'\i}azCaro and Mauro Jaskelioff",
title = "Confluence via strong normalisation in an algebraic $\lambda$calculus with rewriting",
pages = "1629",
year = "2012",
editor = "Simona {Ronchi della Rocca} and Elaine Pimentel",
booktitle = "Proceedings of the 6th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2011)",
series = "Electronic Proceedings in Theoretical Computer Science",
volume = "81",
publisher = "Open Publishing Association"
}

A type system for the vectorial aspect of the linearalgebraic lambdacalculus
(hide)
P. Arrighi, A. DíazCaro, and B. Valiron
 (DCM 2011)  EPTCS 88:115, 2012.
[ EPTCS  COQ proof advertised in the paper  slides ]
doi:10.4204/EPTCS.88.1
We describe a type system for the linearalgebraic lambdacalculus. The type system accounts for the part of the language emulating linear operators and vectors, i.e. it is able to statically describe the linear combinations of terms resulting from the reduction of programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We show that the resulting typed lambdacalculus is strongly normalizing and features a weak subjectreduction.
@InProceedings{ArrighiDiazcaroValironDCM11,
author = "Pablo Arrighi and Alejandro D{\'\i}azCaro and Beno{\^\i}t Valiron",
title = "A type system for the vectorial aspects of the linearalgebraic lambdacalculus",
pages = "115",
year = "2012",
editor = "Elham Kashefi and Jean Krivine and Femke van Raamsdonk",
booktitle = "Proceedings of the 7th International Workshop on Developments of Computational Methods (DCM 2011)",
series = "Electronic Proceedings in Theoretical Computer Science",
volume = "88",
publisher = "Open Publishing Association"
}

Equivalence of algebraic λcalculi  workinprogress
(hide)
A. DíazCaro, S. Perdrix, C. Tasson, and B. Valiron
 HOR 2010, Preproceedings, pp.611, Edinburgh, UK, July 14, 2010
[ arXiv  slides  HOR 2010 site ]
We examine the relationship between the algebraic lambdacalculus λ_{alg}, a fragment of the differential lambdacalculus, and the linearalgebraic lambdacalculus λ_{lin}, a candidate lambdacalculus for quantum computation. Both calculi are algebraic: each one is equipped with an additive and a scalarmultiplicative structure, and the set of terms is closed under linear combinations. We answer the conjectured question of the simulation of λ_{alg} by λ_{lin} and the reverse simulation of λ_{lin} by λ_{alg}. Our proof relies on the observation that λ_{lin} is essentially callbyvalue, while λ_{alg} is callbyname. The former simulation uses the standard notion of thunks, while the latter is based on an algebraic extension of the continuation passing style. This result is a step towards an extension of callbyvalue / callbyname duality to algebraic lambdacalculi
@InProceedings{DiazcaroPerdrixTassonValironHOR10,
author = "Alejandro D{\'\i}azCaro and Simon Perdrix and Christine Tasson and Beno{\^\i}t Valiron",
title = "Equivalence of Algebraic $\lambda$calculi",
booktitle = "Informal proceedings of {HOR}2010",
pages = "611",
year = "2010",
address = "Edinburgh, UK",
month = jul # {~14,},
}

Scalar System F for linearalgebraic λcalculus: Towards a quantum physical logic
(hide)
P. Arrighi and A. DíazCaro
 (QPL 2009)  ENTCS 270(2):219229, 2011.
[ arXiv  ENTCS  slides ]
doi:10.1016/j.entcs.2011.01.033
The LinearAlgebraic LambdaCalculus (arXiv:quantph/0612199) extends the lambdacalculus with the possibility of making arbitrary linear combinations of terms a.t+b.u. Since one can express fixed points over sums in this calculus, one has a notion of infinities arising, and hence indefinite forms. As a consequence, in order to guarantee the confluence, tt does not always reduce to 0  only if t is closed normal. In this paper we provide a System F like type system for the LinearAlgebraic LambdaCalculus, which guarantees normalisation and hence no need for such restrictions, tt always reduces to 0. Moreover this type system keeps track of 'the amount of a type'. As such it can be seen as probabilistic type system, guaranteeing that terms define correct probabilistic functions. It can also be seen as a step along the quest toward a quantum physical logic through the CurryHoward isomorphism.
@InProceedings{ArrighiDiazcaroQPL09,
author = "Pablo Arrighi and Alejandro D{\'\i}azCaro",
title = "Scalar {S}ystem {F} for LinearAlgebraic $\lambda$Calculus: Towards a Quantum Physical Logic",
pages = "206215",
year = "2011",
editor = "Bob Coecke and Prakash Panangaden and Peter Selinger",
booktitle = "Proceedings of the 6th International Workshop on Quantum Physics and Logic ({QPL} 2009)",
series = "Electronic Notes in Theoretical Computer Science",
volume = "270/2",
publisher = "Springer"
}

Measurements and confluence in quantum lambda calculi with explicit qubits
(hide)
P. Arrighi , A. DíazCaro, M. Gadella, and J. J. Grattage
 (QPL/DCM 2008)  ENTCS 270(1):5974, 2011.
[ arXiv  ENTCS ]
doi:10.1016/j.entcs.2011.01.006
This paper demonstrates how to add a measurement operator to quantum lambdacalculi. A proof of the consistency of the semantics is given through a proof of confluence presented in a sufficiently general way to allow this technique to be used for other languages. The method described here may be applied to probabilistic rewrite systems in general, and to add measurement to more complex languages such as QML or Lineal, which is the subject of further research.
@InProceedings{DiazcaroArrighiGadellaGrattageQPLDCM08,
author = "Pablo Arrighi and Alejandro D{\'\i}azCaro and Manuel Gadella and Jonathan J. Grattage",
title = "Measurements and Confluence in Quantum Lambda Calculi With Explicit Qubits",
pages = "5974",
year = "2011",
editor = "Bob Coecke and Ian Mackie and Prakash Panangaden and Peter Selinger",
booktitle = "Proceedings of the Joint 5th International Workshop on Quantum Physics and Logic and 4th Workshop on Developments in Computational Models ({QPL/DCM} 2008)",
series = "Electronic Notes in Theoretical Computer Science",
volume = "270/1",
publisher = "Springer"
}
PhD Thesis

Du typage vectoriel
(hide)
A. DíazCaro. Advisor: P. Arrighi. Coadvisor: F. Prost
 Université de Grenoble, France, Sep. 23, 2011
[ pdf  slides  video (only the dissertation part)  TEL ]
Jury:   
Philippe Jorrand  CNRS  (président) 
Eduardo Bonelli  Universidad Nacional de Quilmes and CONICET  (rapporteur) 
Gilles Dowek  INRIA Centre ParisRocquencourt  (rapporteur) 
Thomas Ehrhard  PPS, Université Paris Diderot  (rapporteur) 
Michele Pagani  LIPN, Université Paris 13  (examinateur) 
Laurent Regnier  IML, Université AixMarseille  (examinateur) 
Lionel Vaux  IML, Université AixMarseille  (examinateur) 
Pablo Arrighi  LIG, Université de Grenoble  (directeur) 
The objective of this thesis is to develop a type theory for the linearalgebraic λcalculus, an extension of λcalculus motivated by quantum computing. This algebraic extension encompass all the terms of λcalculus together with their linear combinations, so if t and r are two terms, so is α.t + β.r, with α and β being scalars from a given ring. The key idea and challenge of this thesis was to introduce a type system where the types, in the same way as the terms, form a vectorial space, providing the information about the structure of the normal form of the terms. This thesis presents the system Lineal, and also three intermediate systems, however interesting by themselves: Scalar, Additive and λCA, all of them with their subject reduction and strong normalisation proofs.
@phdthesis{Diazcaro11,
author = "Alejandro D{\'\i}azCaro",
title = "Du typage vectoriel",
school = "Universit\'e de Grenoble",
year = "2011",
address = "France",
month = sep # {~23,},
}
Master's thesis

Agregando medición al cálculo de van Tonder
(hide)
A. DíazCaro. Advisors M. Gadella and P. E. MartínezLópez
 Universidad Nacional de Rosario, Argentina, Dec. 21, 2007
[ pdf  slides ]
This thesis demonstrates how to add a measurement operator to van Tonder\'s quantum lambdacalculus. Paper [5] is a byproduct of this thesis.
@mastersthesis{Diazcaro07,
author = "Alejandro D{\'\i}azCaro",
title = "Agregando medici\'on al c\'alculo de van Tonder",
school = "Universidad Nacional de Rosario",
year = "2007",
address = "Argentina",
month = dec # {~21,},
}

Universidad Nacional de Quilmes, Bernal, Argentina  Profesor Adjunto

 Lenguajes Formales y Autómatas  Licenciatura en Desarrollo de Software. (2015)
 Características de Lenguajes de Programación  Licenciatura en Desarrollo de Software. (2014)
 Probabilidad y Estadística aplicada a la Bioinformática  Maestría en Bioinformática y Biología de Sistemas. (20142015)

Université Paris Ouest Nanterre La Défense, Nanterre, France  ATER

 Probabilités  TD  L2 Économie et gestion. (2014).
 Statistiques et probabilités  TD  L2 Économie et droit. (2013 & 2014).
 Méthodologie de la mesure en sciences humaines  TD  L1 Psychologie. (2013 & 2014).
 Mathématiques 2  TD  L1 Économie et gestion. (2013 & 2014).
 Mathématiques 1: Calcul et fonctions  TD  L1 Économie et droit. (2012 & 2013).
 Mathématiques 1  TD  L1 Économie et gestion. (2012).

Grenoble INPESISAR, Valence, France  Vacataire

 MA554: Calculabilité et complexité  TD+CM  Cycle Ingénieur  5e année  Informatique et Réseau. (2010).
 MA512: Théorie des graphes  TD+CM  Cycle Ingénieur  5e année  Électronique, Informatique, Systèmes. (2009)

Université Joseph Fourier, Grenoble, France  Vacataire

 INF122B: Compléments mathématiques et introduction à la logique et la preuve formelle  TD  L1 Informatique. (2010).

Universidad Nacional de Rosario, Rosario, Argentina  Ayudante de cátedra

 Algebra y Geometría Analítica I  Ayudante de 1ra  Escuela de Formación Básica. (2008).
 Análisis Matemático I  Ayudante de 1ra  Escuela de Formación Básica. (2008).
 Análisis Matemático IV  Ayudante de 2da  Departamento de Ciencias de la Computación. (2007).


