Prevosto, Virgile Programming Logics, MPI for Informatics, Max Planck Society;
Prevosto, V. (2006). Certified mathematical hierarchies: the FoCal system. In Proceedings of the MAP (Mathematics, Algorithms, Proofs) Workshop. Dagstuhl, Germany: IBFI.