Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Des armes de construction massive : types inductifs et prédicats inductifs