3 papers
cs.LO2008
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic<br> Semantics
Robert Constable, Wojciech Moczydlowski
Church's Higher Order Logic is a basis for influential proof assistants -- HOL and PVS. Church's logic has a simple set-theoretic semantics, making it trustworthy and extensible. W…
cs.LO2007
Normalization of IZF with Replacement
Wojciech Moczydlowski
ZF is a well investigated impredicative constructive version of Zermelo-Fraenkel set theory. Using set terms, we axiomatize IZF with Replacement, which we call \izfr, along with it…
cs.LO2007
A Normalizing Intuitionistic Set Theory with Inaccessible Sets
Wojciech Moczydlowski
We propose a set theory strong enough to interpret powerful type theories underlying proof assistants such as LEGO and also possibly Coq, which at the same time enables program ext…