Initial Semantics for higher-order typed syntax in Coq

Benedikt Ahrens & Zsido, Julianna; Universite' Montpellier II, France
Initial Semantics aims at characterizing the syntax associated to a signature as the initial object of some category. We present an initial semantics result for typed higher-order syntax together with its formalization in the Coq proof assistant. The main theorem was first proved on paper in the second author’s PhD thesis in 2010, and verified formally shortly afterwards. To a simply–typed binding signature S over a fixed set T of object types we associate a...