## Bar recursion

Institutt for informatikk

Universitetet i Bergen

Thursday, 3 February 2011, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B101

**Abstract**: Bar recursion (Spector, 1962) is a principle of
definition by recursion on well-founded trees. These trees are
implicitly defined by a parameter, a second-order aspect from which
bar recursion derives much of its proof-theoretic
strength. Technically, bar recursion is an extension of Gödel's
system T of primitive recursive functionals. We briefly discuss the
semantics of bar recursion, in particular models based on continuity
and majorizability. (The full set-theoretic model of T is not a model
of bar recursion.) Finally, we sketch normalization proofs for bar
recursion. The material of this talk can be found in Chapter 5D of
the forthcoming book *Lambda Calculus with Types* by Barendregt,
Dekkers and Statman (eds.).

Tarmo Uustalu

Last update 18.1.2011