Outline of a proof theory of parametricity

Abstract

Reynolds’ Para λ-calculus (F2), has recently been used by Wadler to prove some unusual and interesting properties of programs. We present a purely syntactic version of the Parametricity Theorem, showing that it is simply an example of formal theorem proving in second order minimal logic over a first order equivalence theory on λ-terms. We analyze the use of parametricity in proving program equivalences, and show that structural induction is still required: parametricity is not enough. As in Leivant’s transparent presentation of Girard’s Representation Theorem for F2, we show that algorithms can be extracted from the proofs, such that if a λ-term can be proven parametric, we can synthesize from the proof an “equivalent” parametric λ-term that is moreover F2-typable. Given that Leivant showed how proofs of termination, based on inductive data types and structural induction, had computational content, we show that inductive data types are indeed parametric, hence providing a connection between the two approaches.