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

Authors: 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}
  }