Abstract

We show a neat set-theoretic semantics for HOL, which works in both constructive and non-constructive settings and which is good enough to describe computational content of constructive HOL proofs.