First- and Second-Order Lambda Calculi with Recursive Types
Recursive types are added to the first- and second-order lambda calculi and the resulting typed terms are shown to be strongly normalizable. A necessary and sufficient condition for strong normalizability is given for unrestricted definitions of recursive types.
computer science; technical report
Previously Published As