Contracts for higher-order functions

Robert Bruce Findler, Matthias Felleisen

Research output: Contribution to journalArticlepeer-review


Assertions play an important role in the construction of robust software. Their use in programming languages dates back to the 1970s. Eiffel, an object-oriented programming language, wholeheartedly adopted assertions and developed the "Design by Contract" philosophy. Indeed, the entire object-oriented community recognizes the value of assertion-based contracts on methods. In contrast, languages with higher-order functions do not support assertion-based contracts. Because predicates on functions are, in general, undecidable, specifying such predicates appears to be meaningless. Instead, the functional languages community developed type systems that statically approximate interesting predicates. In this paper, we show how to support higher-order function contracts in a theoretically well-founded and practically viable manner. Specifically, we introduce λCON, a typed lambda calculus with assertions for higher-order functions. The calculus models the assertion monitoring system that we employ in DrScheme. We establish basic properties of the model (type soundness, etc.) and illustrate the usefulness of contract checking with examples from DrScheme's code base. We believe that the development of an assertion system for higherorder functions serves two purposes. On one hand, the system has strong practical potential because existing type systems simply cannot express many assertions that programmers would like to state. On the other hand, an inspection of a large base of invariants may provide inspiration for the direction of practical future type system research.

Original languageEnglish (US)
Pages (from-to)34-45
Number of pages12
JournalACM SIGPLAN Notices
Issue number4 SUPPL.
StatePublished - Apr 2013


  • Behavioral specifications
  • Contracts
  • Higher-order functions
  • Predicate typing
  • Software reliability

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint Dive into the research topics of 'Contracts for higher-order functions'. Together they form a unique fingerprint.

Cite this