26 June 2015, Theoretical Computer Science Seminar, Rick Statman

Abstract

Type algebras is one of the principal approaches to
recursive types. In this note we generalize this methodology
to give typing schemes which include the usual typing by
recursive and therefore simple types and include as a special
case typings essentially equivalent to Levy labels with strong
normalization and the weak diamond property. These typings are
suitable for proving Chuch-Rosser and standarization of the
untyped case and,in addition, include eta conversion and should
extend to surjective pairing (Stovring's FP, Statman's PSP).
We do this by typing with"paths" of recursive types;
a notion which might berelated to homotopy type theory.

For more information, see http://www.cs.vu.nl/~tcs/seminar.