PRL Seminars

CZF is Peter Aczel's constructive analogue of ZF set theory, and Nuprl-Light is Jason Hickey's framework for specifying, implementing and relating logical systems.

Last week, I presented a translation, due to Aczel, of CZF into type theory. This week, I will outline an approach to implementing this translation as a signature-module relation in Nuprl-Light.