Una de las propiedades fundamentales de la mecánica cuántica es la del no-clonado, la cual indica que es imposible crear una copia idéntica de un estado cuántico desconocido. Los lenguajes funcionales cuánticos pueden diferenciarse dependiendo de cómo se trate dicha propiedad. Por un lado tenemos la familia de lenguajes que utilizan lógica lineal (lenguajes LL) para excluir los términos que duplican estados. Por otro lado tenemos la familia de lenguajes que utilizan propiedades del álgebra lineal (lenguajes AL), los cuales admiten términos que los otros excluyen, pero los interpretan de forma diferente, evitando también el clonado.

Los lenguajes AL, al utilizar un sistema de tipos clásicos, son más sencillos que los LL, pero los primeros tienen una desventaja frente a los últimos: no soportan fácilmente el operador de medición, elemento fundamental de la mecánica cuántica. Por este motivo se propuso desarrollar un lenguaje, λs, que posea lo mejor de ambos enfoques: la elegancia de la linealidad algebraica y el soporte para el operador de medición usando lógica lineal.

El objetivo de la presente tesina es probar la propiedad de normalización fuerte sobre dicho lenguaje. Esta propiedad implica que no habrá loops infinitos, y por lo tanto, un programa bien tipado no tiene ejecuciones infinitas.

Palabras clave: computación cuántica, lambda cálculo, normalización fuerte.