Realizability Interpretation and Normalization of Typed Call-by-Need $$\lambda$$-calculus With Control

TL;DR

This paper introduces a realizability interpretation for a typed call-by-need lambda calculus with control, proving its normalization and extending the approach to a calculus with a classical second-order logic type system.

Contribution

It develops a novel realizability framework for call-by-need lambda calculus with control and extends normalization proofs to a calculus with classical second-order logic.

Findings

Proves normalization of a simply-typed call-by-need calculus with control.

Extends the proof to a calculus with classical second-order predicate logic.

Provides a step towards normalization of call-by-need classical second-order arithmetic.

Abstract

We define a variant of realizability where realizers are pairs of a term and a substitution. This variant allows us to prove the normalization of a simply-typed call-by-need $$\lambda$-$calculus with control due to Ariola et al. Indeed, in such call-by-need calculus, substitutions have to be delayed until knowing if an argument is really needed. In a second step, we extend the proof to a call-by-need $$\lambda$$-calculus equipped with a type system equivalent to classical second-order predicate logic, representing one step towards proving the normalization of the call-by-need classical second-order arithmetic introduced by the second author to provide a proof-as-program interpretation of the axiom of dependent choice.