A Semantic Characterization Of Full Abstraction For Typed Lambda Calculi

Full abstraction is a well known issue in denotational semantics. For a special case of typed lambda calculus, PCF, Plotkin showed that the classical model consisting of domains of continuous functions is not fully abstract. Milner constructed a fully abstract model of typed lambda calculus syntacti...

Full description

Saved in:
Bibliographic Details
Main Author: Mulmuley, K.
Format: Conference Proceeding
Language:English
Subjects:
Aerospace electronics
Calculus
Computer science
Contracts
Mathematical programming
US Department of Defense
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by
cites
container_end_page 288
container_issue
container_start_page 279
container_title
container_volume
creator Mulmuley, K.
description Full abstraction is a well known issue in denotational semantics. For a special case of typed lambda calculus, PCF, Plotkin showed that the classical model consisting of domains of continuous functions is not fully abstract. Milner constructed a fully abstract model of typed lambda calculus syntactically. However, its precise relationship with the classical model was not clear, and hence it remained open whether a fully abstract model can be constructed which is related to the classical model in a pleasant way. In this paper we show that a fully abstract, extensional model of typed lambda calculus can be constructed as a homomorphic retraction of the classical model.
doi_str_mv 10.1109/SFCS.1984.715926
format conference_proceeding
fullrecord <record><control><sourceid>ieee_CHZPO</sourceid><recordid>TN_cdi_ieee_primary_715926</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><ieee_id>715926</ieee_id><sourcerecordid>715926</sourcerecordid><originalsourceid>FETCH-LOGICAL-i157t-fcca0ef5af55c8210c05df28ae4c45b32c67dc929da139d9df472dcd049122b53</originalsourceid><addsrcrecordid>eNotj81Kw0AURgdUsK3uxdW8QOKdydxkZhmCsUKgi1RwV27mB0eStiTpoj69lHb1wTlw4GPsRUAqBJi3tq7aVBit0kKgkfkdW4IWOgc04vueLUAWMkEl9SNbTtMvgAKEbMHWJW_9QPs5Wl790Eh29mP8ozke9nwTeH3qe15203wxF1YfRr49H73jDQ2dI15Rb099fGIPgfrJP992xb7q9221TprNx2dVNkkUWMxJsJbAB6SAaLUUYAFdkJq8sgq7TNq8cNZI40hkxhkXVCGddaCMkLLDbMVer93ovd8dxzjQeN5dT2f_RatLYw</addsrcrecordid><sourcetype>Publisher</sourcetype><iscdi>true</iscdi><recordtype>conference_proceeding</recordtype></control><display><type>conference_proceeding</type><title>A Semantic Characterization Of Full Abstraction For Typed Lambda Calculi</title><source>IEEE Xplore All Conference Series</source><creator>Mulmuley, K.</creator><creatorcontrib>Mulmuley, K.</creatorcontrib><description>Full abstraction is a well known issue in denotational semantics. For a special case of typed lambda calculus, PCF, Plotkin showed that the classical model consisting of domains of continuous functions is not fully abstract. Milner constructed a fully abstract model of typed lambda calculus syntactically. However, its precise relationship with the classical model was not clear, and hence it remained open whether a fully abstract model can be constructed which is related to the classical model in a pleasant way. In this paper we show that a fully abstract, extensional model of typed lambda calculus can be constructed as a homomorphic retraction of the classical model.</description><identifier>ISSN: 0272-5428</identifier><identifier>ISBN: 081860591X</identifier><identifier>ISBN: 9780818605918</identifier><identifier>DOI: 10.1109/SFCS.1984.715926</identifier><language>eng</language><publisher>IEEE</publisher><subject>Aerospace electronics ; Calculus ; Computer science ; Contracts ; Mathematical programming ; US Department of Defense</subject><ispartof>25th Annual Symposium onFoundations of Computer Science, 1984, 1984, p.279-288</ispartof><woscitedreferencessubscribed>false</woscitedreferencessubscribed></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><linktohtml>$$Uhttps://ieeexplore.ieee.org/document/715926$$EHTML$$P50$$Gieee$$H</linktohtml><link.rule.ids>309,310,780,784,789,790,2058,4050,4051,27925,54555,54920,54932</link.rule.ids><linktorsrc>$$Uhttps://ieeexplore.ieee.org/document/715926$$EView_record_in_IEEE$$FView_record_in_$$GIEEE</linktorsrc></links><search><creatorcontrib>Mulmuley, K.</creatorcontrib><title>A Semantic Characterization Of Full Abstraction For Typed Lambda Calculi</title><title>25th Annual Symposium onFoundations of Computer Science, 1984</title><addtitle>SFCS</addtitle><description>Full abstraction is a well known issue in denotational semantics. For a special case of typed lambda calculus, PCF, Plotkin showed that the classical model consisting of domains of continuous functions is not fully abstract. Milner constructed a fully abstract model of typed lambda calculus syntactically. However, its precise relationship with the classical model was not clear, and hence it remained open whether a fully abstract model can be constructed which is related to the classical model in a pleasant way. In this paper we show that a fully abstract, extensional model of typed lambda calculus can be constructed as a homomorphic retraction of the classical model.</description><subject>Aerospace electronics</subject><subject>Calculus</subject><subject>Computer science</subject><subject>Contracts</subject><subject>Mathematical programming</subject><subject>US Department of Defense</subject><issn>0272-5428</issn><isbn>081860591X</isbn><isbn>9780818605918</isbn><fulltext>true</fulltext><rsrctype>conference_proceeding</rsrctype><creationdate>1984</creationdate><recordtype>conference_proceeding</recordtype><sourceid>6IE</sourceid><recordid>eNotj81Kw0AURgdUsK3uxdW8QOKdydxkZhmCsUKgi1RwV27mB0eStiTpoj69lHb1wTlw4GPsRUAqBJi3tq7aVBit0kKgkfkdW4IWOgc04vueLUAWMkEl9SNbTtMvgAKEbMHWJW_9QPs5Wl790Eh29mP8ozke9nwTeH3qe15203wxF1YfRr49H73jDQ2dI15Rb099fGIPgfrJP992xb7q9221TprNx2dVNkkUWMxJsJbAB6SAaLUUYAFdkJq8sgq7TNq8cNZI40hkxhkXVCGddaCMkLLDbMVer93ovd8dxzjQeN5dT2f_RatLYw</recordid><startdate>1984</startdate><enddate>1984</enddate><creator>Mulmuley, K.</creator><general>IEEE</general><scope>6IE</scope><scope>6IL</scope><scope>CBEJK</scope><scope>RIE</scope><scope>RIL</scope></search><sort><creationdate>1984</creationdate><title>A Semantic Characterization Of Full Abstraction For Typed Lambda Calculi</title><author>Mulmuley, K.</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-i157t-fcca0ef5af55c8210c05df28ae4c45b32c67dc929da139d9df472dcd049122b53</frbrgroupid><rsrctype>conference_proceedings</rsrctype><prefilter>conference_proceedings</prefilter><language>eng</language><creationdate>1984</creationdate><topic>Aerospace electronics</topic><topic>Calculus</topic><topic>Computer science</topic><topic>Contracts</topic><topic>Mathematical programming</topic><topic>US Department of Defense</topic><toplevel>online_resources</toplevel><creatorcontrib>Mulmuley, K.</creatorcontrib><collection>IEEE Electronic Library (IEL) Conference Proceedings</collection><collection>IEEE Proceedings Order Plan All Online (POP All Online) 1998-present by volume</collection><collection>IEEE Xplore All Conference Proceedings</collection><collection>IEEE Electronic Library Online</collection><collection>IEEE Proceedings Order Plans (POP All) 1998-Present</collection></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext_linktorsrc</fulltext></delivery><addata><au>Mulmuley, K.</au><format>book</format><genre>proceeding</genre><ristype>CONF</ristype><atitle>A Semantic Characterization Of Full Abstraction For Typed Lambda Calculi</atitle><btitle>25th Annual Symposium onFoundations of Computer Science, 1984</btitle><stitle>SFCS</stitle><date>1984</date><risdate>1984</risdate><spage>279</spage><epage>288</epage><pages>279-288</pages><issn>0272-5428</issn><isbn>081860591X</isbn><isbn>9780818605918</isbn><abstract>Full abstraction is a well known issue in denotational semantics. For a special case of typed lambda calculus, PCF, Plotkin showed that the classical model consisting of domains of continuous functions is not fully abstract. Milner constructed a fully abstract model of typed lambda calculus syntactically. However, its precise relationship with the classical model was not clear, and hence it remained open whether a fully abstract model can be constructed which is related to the classical model in a pleasant way. In this paper we show that a fully abstract, extensional model of typed lambda calculus can be constructed as a homomorphic retraction of the classical model.</abstract><pub>IEEE</pub><doi>10.1109/SFCS.1984.715926</doi><tpages>10</tpages></addata></record>
fulltext fulltext_linktorsrc
identifier ISSN: 0272-5428
ispartof 25th Annual Symposium onFoundations of Computer Science, 1984, 1984, p.279-288
issn 0272-5428
language eng
recordid cdi_ieee_primary_715926
source IEEE Xplore All Conference Series
subjects Aerospace electronics
Calculus
Computer science
Contracts
Mathematical programming
US Department of Defense
title A Semantic Characterization Of Full Abstraction For Typed Lambda Calculi
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2024-12-26T03%3A29%3A26IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-ieee_CHZPO&rft_val_fmt=info:ofi/fmt:kev:mtx:book&rft.genre=proceeding&rft.atitle=A%20Semantic%20Characterization%20Of%20Full%20Abstraction%20For%20Typed%20Lambda%20Calculi&rft.btitle=25th%20Annual%20Symposium%20onFoundations%20of%20Computer%20Science,%201984&rft.au=Mulmuley,%20K.&rft.date=1984&rft.spage=279&rft.epage=288&rft.pages=279-288&rft.issn=0272-5428&rft.isbn=081860591X&rft.isbn_list=9780818605918&rft_id=info:doi/10.1109/SFCS.1984.715926&rft_dat=%3Cieee_CHZPO%3E715926%3C/ieee_CHZPO%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-i157t-fcca0ef5af55c8210c05df28ae4c45b32c67dc929da139d9df472dcd049122b53%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rft_ieee_id=715926&rfr_iscdi=true