Abstract :
Initial Semantics is a categorical framework enabling to abstractly represent and manipulate syntax with binder e.g. lambda calculus, with an appropriate notion of substitution and recursion. This is of important as substitution is famously hard to account properly in a formal setting.
In this talk, we will first consider different approaches that exist in the literature, namely before giving some elements on how the different approaches relates and can be seen as instances of a unified framework.