Context constrained computation

Research output: Contribution to conferencePaper


In normal typed λ-calculi, variables may be used multiple times, in multiple contexts, for multiple reasons, as long as the types agree. The disciplines of linear types and coeffects refine this by tracking how variables are used. For instance, we might track how many times a variable is used, or whether it is used covariantly, contravariantly, or invariantly. Such a discipline yields a general framework of “context constrained computing”, where constraints on variables in the context tell us something interesting about the computation being performed.

We will present work in progress on capturing the “intensional” properties of programs via a family of Kripke indexed relational semantics that refines a simple set-theoretic semantics of programs. The value of our approach lies in its generality and the range of examples covered.
Original languageEnglish
Number of pages2
Publication statusPublished - 27 Sep 2018
Event3rd Workshop on Type-Driven Development (TyDe '18) - St Louis, United States
Duration: 27 Sep 201827 Sep 2018


Workshop3rd Workshop on Type-Driven Development (TyDe '18)
CountryUnited States
CitySt Louis
Internet address


  • computation
  • constraints on variables

Fingerprint Dive into the research topics of 'Context constrained computation'. Together they form a unique fingerprint.

  • Cite this

    Atkey, B., & Wood, J. (2018). Context constrained computation. Paper presented at 3rd Workshop on Type-Driven Development (TyDe '18), St Louis, United States.