## Paper: A fixed point of the second order lambda-calculus: observable equivalences and models (at LICS 1988)

Authors:**Roberto M. Amadio**

### Abstract

The author develops an operational model of an impredicative version of explicit polymorphism, namely, an extension of the second-order lambda-calculus, including a fixed-point combinator and a multisorted first-order algebra. He shows that the typical properties of the λ-calculus are preserved, and he investigates novel aspects that arise from second-order type structure as well as the relationships with well-known, simply typed, PCF-like languages. A suitable theory of observably equivalent terms is defined, and its complexity is explored. A denotional model suggesting interesting extensions of a language is studied

### BibTeX

@InProceedings{Amadio-Afixedpointofthesec, author = {Roberto M. Amadio}, title = {A fixed point of the second order lambda-calculus: observable equivalences and models }, booktitle = {Proceedings of the Third Annual IEEE Symp. on Logic in Computer Science, {LICS} 1988}, year = 1988, editor = {Yuri Gurevich}, month = {July}, pages = {51--60}, location = {Edinburgh, Scotland, UK}, publisher = {IEEE Computer Society Press} }