KnowledgeBase » SEMINAR » ID = 441

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.