Termination of Single-Threaded One-Rule Semi-Thue Systems. - Wojciech Moczydlowski; Alfons Geser (RTA, 2005)

A Dependent Set Theory. - Wojciech Moczydlowski (LICS, 2007)

A Normalizing Intuitionistic Set Theory with Inaccessible Sets. - Wojciech Moczydlowski (Log. Methods Comput. Sci., 2007)

Investigations on Sets and Types. - Wojciech Moczydlowski (2007)

Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics. - Robert L. Constable; Wojciech Moczydlowski (Log. Methods Comput. Sci., 2008)

Normalization of IZF with Replacement. - Wojciech Moczydlowski (Log. Methods Comput. Sci., 2008)

Extracting the resolution algorithm from a completeness proof for the propositional calculus. - Robert L. Constable; Wojciech Moczydlowski (Ann. Pure Appl. Log., 2009)

Unifying sets and programs via dependent types. - Wojciech Moczydlowski (Ann. Pure Appl. Log., 2012)