Abstract types have existential type

Abstract data type declarations appear in typed programming languages like Ada, Alphard, CLU and ML. This form of declaration binds a list of identifiers to a type with associated operations, a composite "value" we call a data algebra. We use a second-order typed lambda calculus SOL to sho...

Full description

Saved in:
Bibliographic Details
Published in:ACM transactions on programming languages and systems 1988-07, Vol.10 (3), p.470-502
Main Authors: Mitchell, John C., Plotkin, Gordon D.
Format: Article
Language:English
Subjects:
Applied sciences
Computer science
control theory
systems
Exact sciences and technology
Formal language definitions
Program semantics
Programming languages
Semantics
Semantics and reasoning
Software
Software and its engineering
Software notations and tools
Theory of computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-a411t-66069b5b54ae8e7f15d2aa4de32330e80ad607003e5df0fa5eb23fa9158700963
cites cdi_FETCH-LOGICAL-a411t-66069b5b54ae8e7f15d2aa4de32330e80ad607003e5df0fa5eb23fa9158700963
container_end_page 502
container_issue 3
container_start_page 470
container_title ACM transactions on programming languages and systems
container_volume 10
creator Mitchell, John C.
Plotkin, Gordon D.
description Abstract data type declarations appear in typed programming languages like Ada, Alphard, CLU and ML. This form of declaration binds a list of identifiers to a type with associated operations, a composite "value" we call a data algebra. We use a second-order typed lambda calculus SOL to show how data algebras may be given types, passed as parameters, and returned as results of function calls. In the process, we discuss the semantics of abstract data type declarations and review a connection between typed programming languages and constructive logic.
doi_str_mv 10.1145/44501.45065
format article
fullrecord <record><control><sourceid>proquest_cross</sourceid><recordid>TN_cdi_proquest_miscellaneous_28877428</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>28877428</sourcerecordid><originalsourceid>FETCH-LOGICAL-a411t-66069b5b54ae8e7f15d2aa4de32330e80ad607003e5df0fa5eb23fa9158700963</originalsourceid><addsrcrecordid>eNo9kE1Lw0AQhhdRsFZPXjz2ULxI6uzHbDbHUvyCghc9L5NkFiPph9mt6L83NqWXGXjnmefwCnEtYSalwXtjEOSsHxZPxEgiusxgoU_FCKQ1GRQKz8VFjJ8AIB26kZjOy5g6qtIk_W45Tj7omyf808TE69RQu48vxVmgNvLVYY_F--PD2-I5W74-vSzmy4yMlCmzFmxRYomG2HEeJNaKyNSsldbADqi2kANoxjpAIORS6UCFRNenhdVjcTt4t93ma8cx-VUTK25bWvNmF71yLs-Ncj14N4BVt4mx4-C3XbOi7tdL8P9N-H0Tft9ET08PWooVtaGjddXE40sORa6U6bGbAaNqdTwOhj-TGGMS</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>28877428</pqid></control><display><type>article</type><title>Abstract types have existential type</title><source>Association for Computing Machinery:Jisc Collections:ACM OPEN Journals 2023-2025 (reading list)</source><creator>Mitchell, John C. ; Plotkin, Gordon D.</creator><creatorcontrib>Mitchell, John C. ; Plotkin, Gordon D.</creatorcontrib><description>Abstract data type declarations appear in typed programming languages like Ada, Alphard, CLU and ML. This form of declaration binds a list of identifiers to a type with associated operations, a composite "value" we call a data algebra. We use a second-order typed lambda calculus SOL to show how data algebras may be given types, passed as parameters, and returned as results of function calls. In the process, we discuss the semantics of abstract data type declarations and review a connection between typed programming languages and constructive logic.</description><identifier>ISSN: 0164-0925</identifier><identifier>EISSN: 1558-4593</identifier><identifier>DOI: 10.1145/44501.45065</identifier><identifier>CODEN: ATPSDT</identifier><language>eng</language><publisher>New York, NY, USA: ACM</publisher><subject>Applied sciences ; Computer science; control theory; systems ; Exact sciences and technology ; Formal language definitions ; Program semantics ; Programming languages ; Semantics ; Semantics and reasoning ; Software ; Software and its engineering ; Software notations and tools ; Theory of computation</subject><ispartof>ACM transactions on programming languages and systems, 1988-07, Vol.10 (3), p.470-502</ispartof><rights>ACM</rights><rights>1989 INIST-CNRS</rights><lds50>peer_reviewed</lds50><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-a411t-66069b5b54ae8e7f15d2aa4de32330e80ad607003e5df0fa5eb23fa9158700963</citedby><cites>FETCH-LOGICAL-a411t-66069b5b54ae8e7f15d2aa4de32330e80ad607003e5df0fa5eb23fa9158700963</cites></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>314,780,784,27924,27925</link.rule.ids><backlink>$$Uhttp://pascal-francis.inist.fr/vibad/index.php?action=getRecordDetail&amp;idt=7097224$$DView record in Pascal Francis$$Hfree_for_read</backlink></links><search><creatorcontrib>Mitchell, John C.</creatorcontrib><creatorcontrib>Plotkin, Gordon D.</creatorcontrib><title>Abstract types have existential type</title><title>ACM transactions on programming languages and systems</title><addtitle>ACM TOPLAS</addtitle><description>Abstract data type declarations appear in typed programming languages like Ada, Alphard, CLU and ML. This form of declaration binds a list of identifiers to a type with associated operations, a composite "value" we call a data algebra. We use a second-order typed lambda calculus SOL to show how data algebras may be given types, passed as parameters, and returned as results of function calls. In the process, we discuss the semantics of abstract data type declarations and review a connection between typed programming languages and constructive logic.</description><subject>Applied sciences</subject><subject>Computer science; control theory; systems</subject><subject>Exact sciences and technology</subject><subject>Formal language definitions</subject><subject>Program semantics</subject><subject>Programming languages</subject><subject>Semantics</subject><subject>Semantics and reasoning</subject><subject>Software</subject><subject>Software and its engineering</subject><subject>Software notations and tools</subject><subject>Theory of computation</subject><issn>0164-0925</issn><issn>1558-4593</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>1988</creationdate><recordtype>article</recordtype><recordid>eNo9kE1Lw0AQhhdRsFZPXjz2ULxI6uzHbDbHUvyCghc9L5NkFiPph9mt6L83NqWXGXjnmefwCnEtYSalwXtjEOSsHxZPxEgiusxgoU_FCKQ1GRQKz8VFjJ8AIB26kZjOy5g6qtIk_W45Tj7omyf808TE69RQu48vxVmgNvLVYY_F--PD2-I5W74-vSzmy4yMlCmzFmxRYomG2HEeJNaKyNSsldbADqi2kANoxjpAIORS6UCFRNenhdVjcTt4t93ma8cx-VUTK25bWvNmF71yLs-Ncj14N4BVt4mx4-C3XbOi7tdL8P9N-H0Tft9ET08PWooVtaGjddXE40sORa6U6bGbAaNqdTwOhj-TGGMS</recordid><startdate>19880701</startdate><enddate>19880701</enddate><creator>Mitchell, John C.</creator><creator>Plotkin, Gordon D.</creator><general>ACM</general><general>Association for Computing Machinery</general><scope>IQODW</scope><scope>AAYXX</scope><scope>CITATION</scope><scope>7SC</scope><scope>8FD</scope><scope>JQ2</scope><scope>L7M</scope><scope>L~C</scope><scope>L~D</scope></search><sort><creationdate>19880701</creationdate><title>Abstract types have existential type</title><author>Mitchell, John C. ; Plotkin, Gordon D.</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-a411t-66069b5b54ae8e7f15d2aa4de32330e80ad607003e5df0fa5eb23fa9158700963</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>1988</creationdate><topic>Applied sciences</topic><topic>Computer science; control theory; systems</topic><topic>Exact sciences and technology</topic><topic>Formal language definitions</topic><topic>Program semantics</topic><topic>Programming languages</topic><topic>Semantics</topic><topic>Semantics and reasoning</topic><topic>Software</topic><topic>Software and its engineering</topic><topic>Software notations and tools</topic><topic>Theory of computation</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Mitchell, John C.</creatorcontrib><creatorcontrib>Plotkin, Gordon D.</creatorcontrib><collection>Pascal-Francis</collection><collection>CrossRef</collection><collection>Computer and Information Systems Abstracts</collection><collection>Technology Research Database</collection><collection>ProQuest Computer Science Collection</collection><collection>Advanced Technologies Database with Aerospace</collection><collection>Computer and Information Systems Abstracts – Academic</collection><collection>Computer and Information Systems Abstracts Professional</collection><jtitle>ACM transactions on programming languages and systems</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Mitchell, John C.</au><au>Plotkin, Gordon D.</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Abstract types have existential type</atitle><jtitle>ACM transactions on programming languages and systems</jtitle><stitle>ACM TOPLAS</stitle><date>1988-07-01</date><risdate>1988</risdate><volume>10</volume><issue>3</issue><spage>470</spage><epage>502</epage><pages>470-502</pages><issn>0164-0925</issn><eissn>1558-4593</eissn><coden>ATPSDT</coden><abstract>Abstract data type declarations appear in typed programming languages like Ada, Alphard, CLU and ML. This form of declaration binds a list of identifiers to a type with associated operations, a composite "value" we call a data algebra. We use a second-order typed lambda calculus SOL to show how data algebras may be given types, passed as parameters, and returned as results of function calls. In the process, we discuss the semantics of abstract data type declarations and review a connection between typed programming languages and constructive logic.</abstract><cop>New York, NY, USA</cop><pub>ACM</pub><doi>10.1145/44501.45065</doi><tpages>33</tpages><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier ISSN: 0164-0925
ispartof ACM transactions on programming languages and systems, 1988-07, Vol.10 (3), p.470-502
issn 0164-0925
1558-4593
language eng
recordid cdi_proquest_miscellaneous_28877428
source Association for Computing Machinery:Jisc Collections:ACM OPEN Journals 2023-2025 (reading list)
subjects Applied sciences
Computer science
control theory
systems
Exact sciences and technology
Formal language definitions
Program semantics
Programming languages
Semantics
Semantics and reasoning
Software
Software and its engineering
Software notations and tools
Theory of computation
title Abstract types have existential type
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2024-12-26T16%3A09%3A49IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Abstract%20types%20have%20existential%20type&rft.jtitle=ACM%20transactions%20on%20programming%20languages%20and%20systems&rft.au=Mitchell,%20John%20C.&rft.date=1988-07-01&rft.volume=10&rft.issue=3&rft.spage=470&rft.epage=502&rft.pages=470-502&rft.issn=0164-0925&rft.eissn=1558-4593&rft.coden=ATPSDT&rft_id=info:doi/10.1145/44501.45065&rft_dat=%3Cproquest_cross%3E28877428%3C/proquest_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-a411t-66069b5b54ae8e7f15d2aa4de32330e80ad607003e5df0fa5eb23fa9158700963%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=28877428&rft_id=info:pmid/&rfr_iscdi=true