PRL Seminars

CZF is a constructive analogue of ZF set theory, and Nuprl-Light is a framework for specifying, implementing, and relating logical systems. I will present a translation of CZF into constructive type theory and then sketch a couple of approaches to implementing this translation as a signature-module relation in Nuprl-Light.

CZF and the translation are due to Peter Aczel [c. 1977]; Nuprl-Light is recent work of Jason Hickey.