Title: A fixed point extension of the second order lambda-calculus: observable equivalences and models
Abstract: We develop 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 multi-sorted first order algebra. We show that typical properties of the X-calculus are preserved and we investigate new aspects that arise by the 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. Eventually a denotational model suggesting interesting extensions of the language is studied.
Publication Year: 1988
Publication Date: 1988-01-01
Language: en
Type: article
Access and Citation
Cited By Count: 7
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot