Well-Typed programs can't be blamed

Philip Wadler*, Robert Bruce Findler

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

92 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationProgramming 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
Pages1-16
Number of pages16
DOIs
StatePublished - 2009
Event18th European Symposium on Programming, ESOP 2009 - York, United Kingdom
Duration: Mar 22 2009Mar 29 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5502
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other18th European Symposium on Programming, ESOP 2009
CountryUnited Kingdom
CityYork
Period3/22/093/29/09

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Well-Typed programs can't be blamed'. Together they form a unique fingerprint.

Cite this