# * CZF, Type Theory, and Nuprl-Light (continued) *

## by Evan Moran

1996-1997

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.