# * (Constructive) set-theoretic semantics for (Constructive) higher-order logic *

## by Wojciech Moczydlowski

2004-2005

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.