Interaction Type Theories

Type systems

A type system is a system which assigns a property called type to every term. Powerful typesystems, such as the Calculus of Constructions, can be used as alternative foundations to mathematics, which can then be used to write proof-checkers which statically verify properties of specific programs.

For example, simply typed lambda calculus is a type system built on top of inference rules. At its core, it has two important inference rules.

x: T; y: U
------------------
(λx:T. y):(T -> U)

x: T -> U; y: T
------------------
(x y): U

This is an informal description; most formal presentations use contexts to accurately specify what these inference rules mean and where and how they can be applied.

It would be desirable to have something like this for the Symmetric Interaction Calculus.

Decomposing type-checking

The first rule of simply-typed lambda calculus looks remarkably like a commutation. We could imagine a term rewriting system where this reduction happens.

<x -> y : T -> U>
-----------------
<x: T> -> <y: U>

This is very similar to the STLC reduction, but backwards. A complex annotation has been reduced into two simple annotations.