On Wednesday 20/11/2013, at 10h30, in room Byron blanc.

**Speaker: ** Herman Geuvers.

**Joint work with: **Bram Geron, Universty of Birmingham.

**Title: ** Types and Data types in Continuation Calculus and lambda calculus.

Abstract:Continuation Calculus (CC), as defined in [1], is a model for functional

computations that aims at (1) being simple (simpler than lambda calculus

and term rewriting), (2) remaining close to actual implementations and

(3) being generic (incorporating various evaluation strategies).

The original system is untyped, but there is a standard procedure for

defining data in CC and writing functions over this data.

In the talk we present a typing system for CC and compare it with the

typing of data in lambda calculus. In lambda calculus, one has the

iterative representation of data (e.g. the Church numerals), but also

the less well-known recursive representation (e.g. the so called “Scott

numerals”). In CC, the recursive data are the “standard” ones and we

show how to type them, compute with them and reason over them.[1] Bram Geron and Herman Geuvers — Continuation calculus,

Proceedings First Workshop on Control Operators and their Semantics,

2013, edited by: Ugo de’Liguoro and Alexis Saurin, EPTCS 127, pp 66-85.