David Ripley

The Curry-Howard correspondence between intuitionistic logic and the simply-typed lambda calculus forms an important bridge between logical and computational research. This talk develops a variant typed lambda calculus, called “core type theory”, that stands in a similar correspondence to Neil Tennant’s “core logic” (fka “intuitionistic relevant logic”), and shows some basic (and some surprising!) results about this calculus.

---