## Paper: Some results on the interpretation of λ-calculus in operator algebras (at LICS 1991)

**Pasquale Malacaria Laurent Regnier**

### Abstract

J.-Y. Girard (Proc. ASL Meeting, 1988) proposed an interpretation of second order λ-calculus in a C algebra and showed that the interpretation of a term is a nilpotent operator. By extending to untyped λ-calculus the functional analysis interpretation for typed λ-terms, V. Danos (Proc. 3rd Italian Conf. on Theor. Comput. Sci., 1989) showed that all and only strongly normalizable terms are interpreted by nilpotent operators; in particular all and only nonstrongly normalizable terms are interpreted by infinite sums of operators. It is shown that interpretation of λ-terms always makes sense, by showing that λ-terms are interpreted by weakly nilpotent operators in the sense of Girard. This result is obtained as a corollary of an aperiodicity property of execution of λ-terms, which seems to be related to some basic property of environment machines

### BibTeX

@InProceedings{MalacariaRegnier-Someresultsontheint, author = {Pasquale Malacaria and Laurent Regnier}, title = {Some results on the interpretation of λ-calculus in operator algebras }, booktitle = {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)}, year = {1991}, month = {July}, pages = {63--72}, location = {Amsterdam, The Netherlands}, publisher = {IEEE Computer Society Press} }