TY - GEN
T1 - Well-Typed programs can't be blamed
AU - Wadler, Philip
AU - Findler, Robert Bruce
PY - 2009
Y1 - 2009
N2 - We introduce the blame calculus, which adds the notion of blame from Findler and Felleisen's contracts to a system similar to Siek and Taha's gradual types and Flanagan's hybrid types. We characterise where positive and negative blame can arise by decomposing the usual notion of subtype into positive and negative subtypes, and show that these recombine to yield naive subtypes. Naive subtypes previously appeared in type systems that are unsound, but we believe this is the first time naive subtypes play a role in establishing type soundness.
AB - We introduce the blame calculus, which adds the notion of blame from Findler and Felleisen's contracts to a system similar to Siek and Taha's gradual types and Flanagan's hybrid types. We characterise where positive and negative blame can arise by decomposing the usual notion of subtype into positive and negative subtypes, and show that these recombine to yield naive subtypes. Naive subtypes previously appeared in type systems that are unsound, but we believe this is the first time naive subtypes play a role in establishing type soundness.
UR - http://www.scopus.com/inward/record.url?scp=67650189558&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=67650189558&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-00590-9_1
DO - 10.1007/978-3-642-00590-9_1
M3 - Conference contribution
AN - SCOPUS:67650189558
SN - 9783642005893
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 16
BT - Programming Languages and Systems - 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, Proceedings
T2 - 18th European Symposium on Programming, ESOP 2009
Y2 - 22 March 2009 through 29 March 2009
ER -