Lambda the Ultimate

A Model for Formal Parametric Polymorphism: A PER Interpretation for System R , Roberto Bellucci, Martin Abadi, Pierre-Louis Curien. TLCA 1995

System R is an extension of system F that formalizes Reynolds' notion of relational parametricity. In system R, considerably more lambda-terms can be proved equal than in system F: for example, the encoded weak products of F are strong products in R. Also, many "theorems for free" à la Wadler can be proved formally in R. In this paper we describe a semantics for system R. As a first step, we give a precise and general reconstruction of the per model of system F of Bainbridge et al., presenting it as a categorical model in the sense of Seely. Then we interpret System R in this model.

System R is a logic for proving relational parametricity results. It's similar in some ways to Abadi-Plotkin logic, which we have linked to previously on LtU.

Cyclic Proofs for First-Order Logic with Inductive Definitions, James Brotherston, in Proceedings of TABLEAUX 2005

We consider a cyclic approach to inductive reasoning in the setting
of first-order logic with inductive definitions. We present a proof
system for this language in which proofs are represented as finite,
locally sound derivation trees with a "repeat function"
identifying cyclic proof sections. Soundness is guaranteed by a
well-foundedness condition formulated globally in terms of
\emph{traces} over the proof tree, following an idea due to Sprenger
and Dam. However, in contrast to their work, our proof system does
not require an extension of logical syntax by ordinal variables.

This technique of making potentially cyclic proof-graphs is really nice since it makes the connection between recursive definitions in a functional programming language and a proof structure very obvious. There is no need to specify the inductive principle ahead of time, you can simply structure the proof tree as you would your functional code.