CZF, Type Theory, and Nuprl-Light (continued)
by Evan Moran
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.