Dinatural Terms in System F

We provide in this article two characterisation results, describing exactly which terms verify the dinaturality diagram, in Church-style system F and in Curry-style system F. The proof techniques we use here are purely syntactic, giving in particular a direct construction of the two terms generated by the dinaturality diagram. But the origin of these techniques lies in fact directly on the analysis of system F through game semantics. Thus, this article provides an example of backward engineering, where powerful syntactic results can be extracted from a semantic analysis.

• Type: Conference
• Year: 2009
• Where: LICS
• Authors: Joachim De Lataillade
• Keywords: Computer Science, Dinaturality Diagram, Direct Construction, LICS 2009, Proof Techniques