Strong Normalization with Non-structural Subtyping. Wand, M., O'Keefe, P., & Palsberg, J. *Mathematical Structures in Computer Science*, 5(3):419-430, September, 1995. Paper abstract bibtex 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.

@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",
}

Downloads: 0

{"_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"]}