Author: Stefano Berardi
Title: Continuations, Backtracking and Limits: A Notion of Construction for Classical Logic
Abstract: 
  We give an overview of a research line started in cooperation with
Prof. Hayashi Proof Animation group. Aim of this research is to describe 
Classical Principle in term of ``constructions'', of a general kind, 
learning a value by trial-and-error, rather than computing it exactly.

  This notion of ``construction'' may be equivalently described in many 
ways. We may use notions from programming: continuations and 
backtracking. We may use notion from game theory: Coquand's game 
interpretation. We may use notions from topology: Hayashi's limit 
interpretation.

  Using this notion of construction, we may define, without using 
Excluded Middle, models of Classical Arithmetic and non-recursive maps. 
These models are algebraic structures, in the ordinary sense: a set of 
individual equipped with maps and a notion of equality.