I am "Investigador Asistente" (Tenured Researcher / Charché de Recherche) at CONICET, since mid 2016, and "Profesor Adjunto con Dedicación Exclusiva" (Tenured Assistant Professor / Maître de Conférences) at Universidad Nacional de Quilmes, since 2014. I belong to 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 January to July 2016 I was a visiting researcher at Universià degli Studi di Torino in the Dipartimento di Informatica, funded by the World Wide Style Project.
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
I was an 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 PhD 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. 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.
In the prehistory I graduated in Computer Science from the Universidad Nacional de Rosario, Argentina in December 2007.
Grants
Publications
International peerreviewed journals

The vectorial λcalculus
(hide)
P. Arrighi, A. DíazCaro, and B. Valiron
 Information and computation 254(1):105139, 2017.
[ arXiv  IC ]
doi:10.1016/j.ic.2017.04.001
We describe a type system for the linearalgebraic
λcalculus. The type system accounts for the linearalgebraic aspects of this extension of λcalculus: 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 λcalculus is strongly normalising and features a weak subject reduction. Finally,
we show how to naturally encode matrices and vectors in this typed calculus.
@Article{ArrighiDiazcaroValironIC17,
author = "Pablo Arrighi and Alejandro D{\'\i}azCaro and Beno\^it Valiron",
title = "The Vectorial LambdaCalculus",
journal = "Information and Computation",
volume = "254",
number= "1",
pages= "105139",
year = "2017"
}

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"
}

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"
}
International peerreviewed conferences

Typing quantum superpositions and measurement
(hide)
A. DíazCaro and G. Dowek
 (TPNC 2017)  To appear in LNCS 10687, 2017.
[ arXiv  Poster (APLAS'17) ]
We propose a way to unify two approaches of noncloning in quantum lambdacalculi. The first approach is to forbid duplicating variables, while the second is to consider all lambdaterms as algebraiclinear functions. We illustrate this idea by defining a quantum extension of firstorder simplytyped lambdacalculus, where the type is linear on superposition, while allows cloning base vectors. In addition, we provide an interpretation of the calculus where superposed types are interpreted as vector spaces and nonsuperposed types as their basis.
@Misc{DiazcaroDowekTPNC17,
author = "D{\'\i}azCaro, Alejandro and Dowek, Gilles",
title = "Typing quantum superpositions and measurement",
year = "2017",
howpublished = "To appear in LNCS 10687 (TPNC 2017). Preprint at {\tt arXiv:1601.04294}",
}

A lambda calculus for density matrices with classical and probabilistic controls
(hide)
A. DíazCaro
 (APLAS 2017)  LNCS 10695:448467, 2017.
[ arXiv  LNCS  slides ]
doi:10.1007/9783319712376_22
In this paper we present two flavors of a quantum extension to the lambda calculus. The first one, λ_{ρ}, follows the approach of classical control/quantum data, where the quantum data is represented by density matrices. We provide an interpretation for programs as density matrices and functions upon them. The second one, λ_{ρ}^{°}, take advantage of the density matrices presentation in order to follow the mixed trace of programs in a kind of generalised density matrix. Such a control can be seen as a weaker form of the quantum control and data approach.
@InProceedings{DiazcaroAPLAS17,
author = "Alejandro D{\'\i}azCaro",
title = "A lambda calculus for density matrices with classical and probabilistic controls",
booktitle = "Programming Languages and Systems (APLAS 2017)",
editor = "BorYuh Evan Chang",
series = "Lecture Notes in Computer Science",
publisher = "Springer Berlin Heidelberg",
pages = "448467",
volume = "10695",
year = "2017"
}

Affine computation and affine automaton
(hide)
A. DíazCaro and A. Yakaryılmaz
 (CSR 2016)  LNCS 9691:146160, 2016.
[ arXiv  LNCS  slides ]
doi:10.1007/9783319341712_11
We introduce a quantumlike classical computational model, called affine computation, as a generalization of probabilistic computation. After giving the basics of affine computation, we define affine finite automata (AfA) and compare it with quantum and probabilistic finite automata (QFA and PFA, respectively) with respect to three basic language recognition modes. We show that, in the cases of bounded and unbounded error, AfAs are more powerful than QFAs and PFAs, and, in the case of nondeterministic computation, AfAs are more powerful than PFAs but equivalent to QFAs.
@InProceedings{DiazcaroYakaryilmazCSR16,
author = "Alejandro D\'iazCaro and Abuzer Yakary\ilmaz ",
title = "Affine computation and affine automaton",
booktitle = "Computer Science  Theory and Applications: 11th International Computer Science Symposium in Russia (CSR 2016)",
editor = "Alexander Kulikov and Gerhard Woeginger",
series = "Lecture Notes in Computer Science",
publisher = "Springer Berlin Heidelberg",
pages = "146160",
volume = "9691",
year = "2016"
}

Isomorphisms considered as equalities
Projecting functions and enhancing partial application through an implementation of λ⁺
(hide)
A. DíazCaro 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
We propose an implementation of λ⁺, a recently introduced simply typed lambdacalculus with pairs where isomorphic types are made equal. The rewrite system of λ⁺ is a rewrite system modulo an equivalence relation, which makes its implementation nontrivial. We also extend λ⁺ with natural numbers and general recursion and use Bekić's theorem to split mutual recursions. This splitting, together with the features of λ⁺, allows for a novel way of program transformation by reduction, by projecting a function before it is applied in order to simplify it. Also, currying together with the associativity and commutativity of pairs gives an enhanced form of partial application.
@InProceedings{DiazcaroMartinezlopezIFL15,
author = "D\'iazCaro, Alejandro and Mart\'inez L\'opez, Pablo E.",
title = "Isomorphisms considered as equalities: Projecting functions and enhancing partial application through an implementation of $\lambda^+$",
booktitle = "Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages",
series = "IFL '15",
publisher = "ACM",
pages = "9:19:11",
articleno = "9",
year = "2015",
}

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"
}

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"
}
International peerreviewed workshops

Confluence in probabilistic rewriting
(hide)
A. DíazCaro and G. Martínez
 (LSFA 2017)  Submitted to ENTCS, 2017.
[ arXiv ]
Driven by the interest of reasoning about probabilistic programming languages, we set out to study a notion of unicity of normal forms for them. To provide a tractable proof method for it, we define a property of distribution confluence which is shown to imply the desired unicity and further properties. We then carry over several criteria from the classical case, such as Newman’s lemma, to simplify proving confluence in concrete languages. Using these criteria, we obtain simple proofs of confluence for λ_{1}, an affine probabilistic λcalculus, and for Q*, a quantum programming language for which a related property has already been proven in the literature. Lastly, we show how distribution confluence implies unicity even for distributions that are only reached asymptotically.
@Misc{DiazcaroMartinezLSFA17,
author = "Alejandro D{\'\i}azCaro and Guido Mart{\'\i}nez",
title = "Confluence in probabilistic rewriting",
year = "2017",
howpublished = "Preproceedings of LSFA 2017. Preprint at {\tt arXiv:1708.03536}."
}

Retractions in intersection types
(hide)
M. Coppo, M. DezaniCiancaglini, A. DíazCaro, I. Margaria and M. Zacchi 
(ITRS 2016)  EPTCS 242:3147, 2017.
[ EPTCS ]
doi:10.4204/EPTCS.242.5
This paper discusses retraction—intended as isomorphic embedding—in intersection types building left and right inverses as terms of a lambdacalculus with a bottom constant. The main result is a necessary and sufficient condition two types must satisfy in order to assure the existence of two terms showing the first type to be a retract of the second one.
@InProceedings{CoppoDezaniciancagliniDiazcaroMargariaZacchiITRS16,
author = "Mario Coppo, Mariangiola DezaniCiancaglini, Alejandro D\'{\i}azCaro, Ines Margaria, Maddalena Zacchi",
title = "Retractions in intersection types",
pages = "3147",
year = "2017",
editor = "Naoki Kobayashi",
booktitle = "Proceedings Eighth Workshop on Intersection Types and Related Systems",
series = "Electronic Proceedings in Theoretical Computer Science",
volume = "242",
publisher = "Open Publishing Association"
}

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"
}

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"
}

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 ]
doi:10.13140/RG.2.1.2528.4961
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"
}
Theses

Du typage vectoriel
(hide)  PhD Thesis
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,},
}

Agregando medición al cálculo de van Tonder
(hide)  Master's Thesis
A. DíazCaro. Advisors M. Gadella and P. E. Martínez Ló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,},
}
Science popularisation
Drafts

Simply typed lambdacalculus modulo type isomorphisms
(hide)
A. DíazCaro and G. Dowek
 hal01109104  2016
[ HAL (Draft)  Slides at TYPES'14 ]
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{DiazcaroDowek16,
author = "Alejandro D{\'\i}azCaro and Gilles Dowek",
title = "Simply typed lambdacalculus modulo type isomorphisms",
year = "2016",
howpublished = "Draft at https://hal.inria.fr/hal01109104"
}
