Dr. Wojciech Moczydlowski won the Sacks Prize from the Association for Symbolic Logic for his thesis Investigations on Sets and Types. Wojtek's work created a new way to analyze constructive set theories and relate them to type theory. His work makes it possible to share formal results produced by set theory based theorem provers such as Mizar and B with the type theory based provers such as Coq, HOL, Nuprl.