Verifying higher-order functional programs with pattern-matching algebraic data types.

C.-H. Luke Ong, Steven J. Ramsay

Browse the full POPL paper archive.