@Article{WandOKeefePalsberg95,
  author = 	"Mitchell Wand and Patrick O'Keefe and Jens Palsberg",
  title = 	"Strong Normalization with Non-structural Subtyping",
  journal = 	"Mathematical Structures in Computer Science",
  year = 1995,		 
  volume = 	"5",
  number = 	"3",
  pages = 	"419-430",
  month = 	sep,
  abstract =    "We study a type system with a notion of subtyping 
that involves a largest type $\top$, a smallest type $\bot$, 
atomic coercions between base types, 
and the usual ordering of function types.
We prove that any $\lambda$-term typable in this system 
is strongly normalizing; this solves an open problem of Thatte.
We also prove that the fragment without $\bot$ types strictly fewer terms.
This demonstrates that $\bot$ adds power to a type system.",
  source = {~/types/sn/final.tex},
  URL =	 "ftp://ftp.ccs.neu.edu/pub/people/wand/papers/w-ok-p-94.dvi",
}

{"_id":"HbFYb24qae2Wk4Q7h","bibbaseid":"wand-okeefe-palsberg-strongnormalizationwithnonstructuralsubtyping-1995","downloads":0,"creationDate":"2017-04-23T20:31:12.579Z","title":"Strong Normalization with Non-structural Subtyping","author_short":["Wand, M.","O'Keefe, P.","Palsberg, J."],"year":1995,"bibtype":"article","biburl":"http://www.ccs.neu.edu/home/wand/Bibliography.bib","bibdata":{"bibtype":"article","type":"article","author":[{"firstnames":["Mitchell"],"propositions":[],"lastnames":["Wand"],"suffixes":[]},{"firstnames":["Patrick"],"propositions":[],"lastnames":["O'Keefe"],"suffixes":[]},{"firstnames":["Jens"],"propositions":[],"lastnames":["Palsberg"],"suffixes":[]}],"title":"Strong Normalization with Non-structural Subtyping","journal":"Mathematical Structures in Computer Science","year":"1995","volume":"5","number":"3","pages":"419-430","month":"September","abstract":"We study a type system with a notion of subtyping that involves a largest type $\\top$, a smallest type $\\bot$, atomic coercions between base types, and the usual ordering of function types. We prove that any $\\lambda$-term typable in this system is strongly normalizing; this solves an open problem of Thatte. We also prove that the fragment without $\\bot$ types strictly fewer terms. This demonstrates that $\\bot$ adds power to a type system.","source":"~/types/sn/final.tex","url":"ftp://ftp.ccs.neu.edu/pub/people/wand/papers/w-ok-p-94.dvi","bibtex":"@Article{WandOKeefePalsberg95,\n author = \t\"Mitchell Wand and Patrick O'Keefe and Jens Palsberg\",\n title = \t\"Strong Normalization with Non-structural Subtyping\",\n journal = \t\"Mathematical Structures in Computer Science\",\n year = 1995,\t\t \n volume = \t\"5\",\n number = \t\"3\",\n pages = \t\"419-430\",\n month = \tsep,\n abstract = \"We study a type system with a notion of subtyping \nthat involves a largest type $\\top$, a smallest type $\\bot$, \natomic coercions between base types, \nand the usual ordering of function types.\nWe prove that any $\\lambda$-term typable in this system \nis strongly normalizing; this solves an open problem of Thatte.\nWe also prove that the fragment without $\\bot$ types strictly fewer terms.\nThis demonstrates that $\\bot$ adds power to a type system.\",\n source = {~/types/sn/final.tex},\n URL =\t \"ftp://ftp.ccs.neu.edu/pub/people/wand/papers/w-ok-p-94.dvi\",\n}\n\n","author_short":["Wand, M.","O'Keefe, P.","Palsberg, J."],"key":"WandOKeefePalsberg95","id":"WandOKeefePalsberg95","bibbaseid":"wand-okeefe-palsberg-strongnormalizationwithnonstructuralsubtyping-1995","role":"author","urls":{"Paper":"ftp://ftp.ccs.neu.edu/pub/people/wand/papers/w-ok-p-94.dvi"},"downloads":0,"html":""},"search_terms":["strong","normalization","non","structural","subtyping","wand","o'keefe","palsberg"],"keywords":[],"authorIDs":[],"dataSources":["zM8mNPR4ZkAHKtvDs"]}