Skip to main content
PRL Project

(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.