The simply-typed lambda calculus is modeled by any cartesian closed category. That means we can define categories representing domain specific interpretations such as hardware circuits or automatic differentiation, and then execute existing programs on them (in this case written in GHC Haskell.)
