TYPES is a moderated email forum focusing on Type Theory in Computer Science, with a broad view of the subject encompassing semantical, categorical, operational, and proof theoretical topics. Typical topics include:
Typed, untyped, or polymorphic lambda calculus; type checking, inference, and reconstruction; dependent types, calculus of constructions, the lambda cube; linear logic, the CurryHoward correspondence; recursive types; adequate and fully abstract models; domain theory; category theory; term reduction, strong normalization, confluence; abstract data types, type systems for objectoriented programming.
Needless to say, type theory is quite important programming language research. In fact, you might say it is its coner stone.
A good introduction to most of these topics can be found in the papers of Luca Cardelli
Posted to "" by Ehud Lamm on 9/10/00; 11:49:26 AM

