Log in to Zulip

This Zulip chat (public archives) lives alongside the types-list mailing-list:

TYPES is a discussion forum focusing on Type Theory in Computer Science, with a broad view of the subject encompassing semantical, categorical, operational, and proof theoretical topics, as well as algorithmic issues and applications.

Typical topics include: typed, untyped, or polymorphic lambda calculus; type checking, inference, and reconstruction; subtyping, dependent types, calculus of constructions, the lambda cube; linear logic, the Curry-Howard correspondence; recursive types; adequate and fully abstract models; domain theory; category theory; term reduction, normalization, confluence; abstract data types; type systems for object-oriented, concurrent, distributed, and mobile programming.

Comments and criticisms of results in the literature, open problems, and research queries are encouraged.