Ranzi, Florian (2015) From a Flexible Type System to Metapredicative Wellordering Proofs thesis, Institut für Informatik und angewandte Mathematik.