Recent Papers on Realizability and Related Topics

On this page I aim to collect links to recent, published and unpublished papers connected to realizability. Have you written anything new, and do you wish it to be included, send me the URL where it can be downloaded.

Federico Aschieri

Learning, Realizability and Games in Classical Arithmetic (pdf), Ph.D. thesis, March-April 2011

Steven Awodey and Andrej Bauer

Sheaf Toposes for Realizability (pdf), Archive for Mathematical Logic 47,5 (2008),465--478.

Andrej Bauer

The Realizability Approach to Computable Analysis and Topology, thesis.

On the Failure of Fixed-Point Theorems for Chain-complete Lattices in the Effective Topos.

Benno van den Berg and Claire Kouwenhoven

W-Types in the Effective Topos, note.

Benno van den Berg and Ieke Moerdijk

Aspects of Predicative Algebraic Set Theory II: Realizability, to appear in TCS.

Benno van den Berg and Jaap van Oosten

Arithmetic is Categorical, May 2011. Submitted to TAC.

Bodil Biering

Dialectica Interpretations - A Categorical Analysis, thesis.

Lars Birkedal and Jaap van Oosten

Relative and Modified Relative Realizability, Annals of Pure and Applied Logic 118 (2002), 115-132

Wolfgang Burr

Concepts and Aims of Functional Interpretations (ps format), in: Löwe and Rudolph (eds), Foundations of the Formal Sciences, Kluwer 1999, pp.205--218

The intuitionistic arithmetical hierarchy, Logic Colloquium '99, pp. 51--59, Lect. Notes Log. 17.

Fragments of Heyting Arithmetic (ps format), J. Symbolic Logic 65 (2000), no. 3, 1223--1240.

J.R.B. Cockett and P.W. Hofstra

Introduction to Turing Categories, APAL 156,2-3 (2008),183--209.

Eric Faber and Jaap van Oosten

Effective Operations of Type 2 in PCAs. Submitted.

More on Geometric Morphisms between Realizability Toposes. Submitted.

Fernando Ferreira and Ana Nunes

Bounded Modified Realizability, Journal of Symbolic Logic 71 (2006), 329--346

Martin Hofmann, Jaap van Oosten and Thomas Streicher

Well-foundedness in Realizability

Archive for Mathematical Logic 45 (2006), 795--805

Pieter Hofstra

Relative Completions, JPAA 192, 1-3 (2004), 129--148

Completions in Realizability (Thesis)

All realizability is relative, Math.Proc.Camb.Phil.Soc. 141 (2006), 239--264

Pieter Hofstra and Jaap van Oosten

Ordered PCA's, Math.Proc.Camb.Phil.Soc.134 (2003),445-463.

Erratum to "Ordered PCA's"

Martin Hyland

Variations on Realizability--ps.gz file,Math.Struct.Comp.Sci. 12 (2002)

Claire Kouwenhoven-Gentil and Jaap van Oosten

Algebraic Set Theory and the Effective Topos--ps.gz file, Journ.Symb.Log.70(3) (2005),879-890

Sori Lee and Jaap van Oosten

Basic Subtoposes of the Effective Topos--pdf file. Annals of Pure and Applied Logic 164 (2013), 866-883

Peter Lietz

Comparing Realizability over Pw and K2--ps.gz file

Peter Lietz and Thomas Streicher

Impredicativity entails Untypedness--ps.gz file

Peter Lietz

From constructive mathematics to computable analysis via the realizability interpretation (PhD thesis)--link to pdf

John Longley

Realizability toposes and language semantics, thesis (1995), University of Edinburgh, available as ECS-LFCS-95,332

Unifying Typed and Untyped Realizability, note--text file

The sequentially realizable functionals, APAL 117,1-3 (2002),1--93. pdf file.

On the ubiquity of certain total type structures, MSCS 17,5 (2007),841--953. pdf file.

Computability structures, simulations and realizability, May 2011, pdf file.

John Longley and Alex Simpson

A uniform approach to domain theory in realizability models. MSCS 7 (1997), 469--505.

F. de Marchi, E. Robinson and G. Rosolini

An abstract look at realizability--ps file, final version published by Robinson and Rosolini in CSL 2001, LNCS 2142.

M. Marz, A. Rohr and T. Streicher

Full Abstraction and Universality via Realisability--ps.gz file

S. Maschio and T. Streicher

Models of Intuitionistic Set Theory in Subtoposes of Nested Realizability Toposes--pdf file

Matías Menni

A Characterization of the Left Exact Categories whose Exact Completions are Toposes--link.
Journal of pure and applied algebra 177, 287-301, 3, 2003.

Exact Completions and Toposes, thesis--pdf file

Läuchli's Completeness Theorem from a Topos-theoretic perspective, Applied Categorical Structures 2008.

Alexandre Miquel

A Strongly Normalising Curry-Howard Correspondence for IZF Set Theory pdf file
Also in: CSL 2003, pp.441-454.

Wojciech Moczydlowski

Normalization of IZF with Replacement ps file
Also (shorter) in: CSL 2006,LNCS 4207 (Springer), pp.516--530

Joan Rand Moschovakis

Hierarchies in Intuitionistic Arithmeticps file

Classical and Intuitionistic Hierarchies in Extended Intuitionistic Analysisps file

Jaap van Oosten

Realizability: a historical essay, Math.Struct.Comp.Sci. 12 (2002), 239-263

A Partial Analysis of Modified Realizability, Journ.Symb.Log. 69 (2004),2,421-429

Filtered Colimits in the Effective Topos Journ. Pure Appl.Alg. 205 (2006), 446--451

A general form of relative recursion,Notre Dame Journal od Formal Logic 47(3) (2006), 311-318

Partial Combinatory Algebras of Functions, Notre Dame Journal of Formal Logic 52(4) (2011), 431-448

A notion of Homotopy for the Effective Topos, March 2010.

Realizability with a Local Operator of A.M. Pitts, Theoretical Computer Science 546 (2014), 237-243.

Andrew Pitts

The Theory of Triposes, Ph.D. thesis, Cambridge 1981.

Tripos Theory in Retrospect,Math.Struct.Comp.Sci. 12 (2002).

Michael Rathjen

CZF has the Disjunction and Numerical Existence Property,Journal of Symbolic Logic 70 (2005) 1233-1254.

Constructive set theory and Brouwerian principles, Journal of Universal Computer Science, Vol. 11, No. 12 (2005) 2008-2033.

Choice principles in constructive and classical set theories, Lecture Notes in Logic 27 (2006) 299-326.

Realizability for Constructive Zermelo-Fraenkel Set Theory, Logic Colloquium 2003. Lecture Notes In Logic 141 (2006) 442-471.

Metamathematical Properties of Intuitionistic Set Theories with Choice Principles, in: Cooper, Loewe, Sorbi: New Computational Paradigms (Springer 2008) 84-98.

Frédéric Ruyer

Preuves, Types et Sous-Types, thesis, ps file.

Alex Simpson

Solving Recursive Domain Equations in Models of Intuitionistic Set Theory--ps.gz file

Wouter Stekelenburg

A Note on ``Extensional PERs''--pdf file, J. Pure Appl. Algebra 215 (2011), no. 3, 253–256.

Regular Functors and Relative Realizability Categories--pdf file, accepted for MSCS

Realizability Catgories--pdf file, thesis.(submitted).

Thomas Streicher

A Semantic Version of the Diller-Nahm Variant of Gödel's Dialectica Interpretation--ps.gz file

Krivine's Classical Realizability from a Categorical Perspective pdf file

A Classical Realizability Model arising from a Stable Model of Untyped Lambda Calculus pdf file

Albert Ziegler

Generalising Realizability and Heyting Models for Constructive Set Theory--pdf document; talk presented at 3d Workshop on Formal Topology, Padova, May 2007

Diplomarbeit (in German), München 2007


To Jaap van Oosten.