English

Structures de r\'ealisabilit\'e, RAM et ultrafiltre sur N

Logic in Computer Science 2008-09-16 v1

Abstract

We show how to transform into programs the proofs in classical Analysis which use the existence of an ultrafilter on the integers. The method mixes the classical realizability introduced by the author, with the "forcing" of P. Cohen. The programs we obtain, use read and write instructions in random access memory.

Keywords

Cite

@article{arxiv.0809.2394,
  title  = {Structures de r\'ealisabilit\'e, RAM et ultrafiltre sur N},
  author = {Jean-Louis Krivine},
  journal= {arXiv preprint arXiv:0809.2394},
  year   = {2008}
}

Comments

34 p

R2 v1 2026-06-21T11:20:04.275Z