Recursive proofs for inductive tree data-structures.

Parthasarathy Madhusudan, Xiaokang Qiu, Andrei Stefanescu

Browse the full POPL paper archive.