FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Classical realizability as a classifier for nondeterminism

Author: Guillaume Geoffroy

Paper Information

Title:Classical realizability as a classifier for nondeterminism
Authors:Guillaume Geoffroy
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:classical realizability, nondeterminism, boolean algebra, realizability, proof-as-program, Curry-Howard
Abstract:

ABSTRACT. We show how the language of Krivine's classical realizability may be used to specify various forms of nondeterminism and relate them with properties of realizability models. More specifically, we introduce an abstract notion of multi-evaluation relation which allows us to finely describe various nondeterministic behaviours. This defines a hierarchy of computational models, ordered by their degree of nondeterminism, similar to Sazonov's degrees of parallelism. What we show is a duality between the structure of the characteristic boolean algebra of a realizability model and the degree of nondeterminism in its underlying computational model.

Pages:10
Talk:Jul 10 12:20 (Session 54E)
Paper: