@InProceedings{Wand85a,
  author = 	"Wand, Mitchell",
  title = 	"Embedding Type Structure in Semantics",
  booktitle = 	"{\popl{12th}}",
  year = 	"1985",
  pages = 	"1--6",
  source =  {/proj/wand/old/popl85/paper.tex},
  URL = {ftp://ftp.ccs.neu.edu/pub/people/wand/papers/popl-85.ps},	  
  abstract = "We show how a programming language designer may embed
the type structure of of a programming language in the more robust
type structure of the typed lambda calculus.  This is done by
translating programs of the language into terms of the typed lambda
calculus.  Our translation, however, does not always yield a
well-typed lambda term.  Programs whose translations are not
well-typed are considered meaningless, that is, ill-typed.  We give a
conditionally type-correct semantics for a simple language with
continuation semantics.  We provide a set of static type-checking
rules for our source language, and prove that they are sound and
complete: that is, a program passes the typing rules if and only if
its translation is well-typed.  This proves the correctness of our
static semantics relative to the well-established typing rules of the
typed lambda-calculus."  }

{"_id":"icFkdw4JrZeha7ZiY","bibbaseid":"wand-embeddingtypestructureinsemantics-1985","downloads":0,"creationDate":"2017-04-23T20:31:12.539Z","title":"Embedding Type Structure in Semantics","author_short":["Wand, M."],"year":1985,"bibtype":"inproceedings","biburl":"http://www.ccs.neu.edu/home/wand/Bibliography.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Wand"],"firstnames":["Mitchell"],"suffixes":[]}],"title":"Embedding Type Structure in Semantics","booktitle":"\\popl12th","year":"1985","pages":"1--6","source":"/proj/wand/old/popl85/paper.tex","url":"ftp://ftp.ccs.neu.edu/pub/people/wand/papers/popl-85.ps","abstract":"We show how a programming language designer may embed the type structure of of a programming language in the more robust type structure of the typed lambda calculus. This is done by translating programs of the language into terms of the typed lambda calculus. Our translation, however, does not always yield a well-typed lambda term. Programs whose translations are not well-typed are considered meaningless, that is, ill-typed. We give a conditionally type-correct semantics for a simple language with continuation semantics. We provide a set of static type-checking rules for our source language, and prove that they are sound and complete: that is, a program passes the typing rules if and only if its translation is well-typed. This proves the correctness of our static semantics relative to the well-established typing rules of the typed lambda-calculus.","bibtex":"@InProceedings{Wand85a,\n author = \t\"Wand, Mitchell\",\n title = \t\"Embedding Type Structure in Semantics\",\n booktitle = \t\"{\\popl{12th}}\",\n year = \t\"1985\",\n pages = \t\"1--6\",\n source = {/proj/wand/old/popl85/paper.tex},\n URL = {ftp://ftp.ccs.neu.edu/pub/people/wand/papers/popl-85.ps},\t \n abstract = \"We show how a programming language designer may embed\nthe type structure of of a programming language in the more robust\ntype structure of the typed lambda calculus. This is done by\ntranslating programs of the language into terms of the typed lambda\ncalculus. Our translation, however, does not always yield a\nwell-typed lambda term. Programs whose translations are not\nwell-typed are considered meaningless, that is, ill-typed. We give a\nconditionally type-correct semantics for a simple language with\ncontinuation semantics. We provide a set of static type-checking\nrules for our source language, and prove that they are sound and\ncomplete: that is, a program passes the typing rules if and only if\nits translation is well-typed. This proves the correctness of our\nstatic semantics relative to the well-established typing rules of the\ntyped lambda-calculus.\" }\n\n","author_short":["Wand, M."],"key":"Wand85a","id":"Wand85a","bibbaseid":"wand-embeddingtypestructureinsemantics-1985","role":"author","urls":{"Paper":"ftp://ftp.ccs.neu.edu/pub/people/wand/papers/popl-85.ps"},"downloads":0,"html":""},"search_terms":["embedding","type","structure","semantics","wand"],"keywords":[],"authorIDs":["58fd0f10bfc623c939000018"],"dataSources":["zM8mNPR4ZkAHKtvDs"]}