לירון כהן

Church–Turing computability, which is the standard notion of computation, is based on functions for which there is an effective method for constructing their values. However, intuitionistic mathematics, as conceived by Brouwer, extends the notion of effective algorithmic constructions by also admitting constructions corresponding to human experiences of mathematical truths, which are based on temporal intuitions. In particular, the key notion of infinitely proceeding sequences of freely chosen objects, known as free choice sequences, regards functions as being constructed over time. This paper describes how free choice sequences can be embedded in an implemented formal framework, namely the constructive type theory of the Nuprl proof assistant. Some broader implications of supporting such an extended notion of computability in a formal system are then discussed, focusing on formal verification and constructive mathematics.