Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Second Annual IEEE Symposium on

Logic in Computer Science (LICS 1987)

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

Last modified: 2018-06-2121:59
Andrzej Murawski