Typed vs. Untyped Realizability

We study the domain-theoretic semantics of a Church-style typed λ-calculus with constructors, pattern matching and recursion, and show that it is closely related to the semantics of its untyped counterpart. The motivation for this study comes from program extraction from proofs via realizability where one has the choice of extracting typed or untyped terms from proofs. Our result shows that under a certain regularity condition, the choice is irrelevant. The regularity condition is that in every use of a fixed point type fix α.ρ, α occurs only positively in ρ.