INVESTIGADORES
DÍAZ CARO Alejandro
artículos
Título:
Linearity in the non-deterministic call-by-value setting
Autor/es:
ALEJANDRO DÍAZ CARO; BARBARA PETIT
Revista:
LECTURE NOTES IN COMPUTER SCIENCE
Editorial:
Springer-Verlag
Referencias:
Lugar: Berlín; Año: 2012 vol. 7456 p. 216 - 231
ISSN:
0302-9743
Resumen:
We consider the non-deterministic extension of the call-by-value lambda calculus, which corresponds to the additive fragment of the linear-algebraic lambda-calculus. We define a fine-grained 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.
