Complete monitors for gradual types

Ben Greenman, Matthias Felleisen, Christos Dimoulas

Research output: Contribution to journalArticlepeer-review

5 Scopus citations


In the context of gradual typing, type soundness guarantees the safety of typed code. When untyped code fails to respect types, a runtime check finds the discrepancy. As for untyped code, type soundness makes no promises; it does not protect untyped code from mistakes in type specifications and unwarranted blame. To address the asymmetry, this paper adapts complete monitoring from the contract world to gradual typing. Complete monitoring strengthens plain soundness into a guarantee that catches problems with faulty type specifications. Furthermore, a semantics that satisfies complete monitoring can easily pinpoint the conflict between a type specification and a value. For gradual typing systems that fail complete monitoring, the technical framework provides a source-of-truth to assess the quality of blame.

Original languageEnglish (US)
Article numberA122
JournalProceedings of the ACM on Programming Languages
Issue numberOOPSLA
StatePublished - Oct 2019


  • Blame completeness
  • Blame soundness
  • Complete monitoring

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality


Dive into the research topics of 'Complete monitors for gradual types'. Together they form a unique fingerprint.

Cite this