## Paper: Recursive Types and Type Constraints in Second-Order Lambda Calculus (at LICS 1987)

**Nax P. Mendler**

### Abstract

We add to the second-order lambda calculus type constructors
μ and ν, which give the least and greatest solutions to positively
defined type expressions. Strong normalizability of typed terms is shown using
Girad's *candidates for reduction* method. Using the same structure built
for that proof, we prove a necessary and sufficient condition for when a
collection of type constraints admit the typing of only strongly normalizable terms.

### BibTeX

@InProceedings{Mendler-RecursiveTypesandTy, author = {Nax P. Mendler}, title = {Recursive Types and Type Constraints in Second-Order Lambda Calculus}, booktitle = {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)}, year = {1987}, month = {June}, pages = {30--36}, location = {Ithaca, NY, USA}, publisher = {IEEE Computer Society Press} }