Search

• < Previous
• 1
• Next >

On the Semantic Expressiveness of Iso- and Equi-Recursive Types

Recursive types extend the simply-typed lambda calculus (STLC) with the additional expressive power to enable diverging computation and to encode recursive data-types (e.g., lists). Two formulations of recursive types exist: iso-recursive and equi-recursive. The relative advantages of iso- and&nbsp;[&hellip;]