Catherine Parent: Synthesizing Proofs from Programs in the Calculus of Inductive Constructions. MPC 1995: 351-379