Jean-François Monin: Extracting Programs with Exceptions in an Impredicative Type System. MPC 1995: 335-350