Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums.

Vincent Balat, Roberto Di Cosmo, Marcelo P. Fiore

Browse the full POPL paper archive.