The goal of this talk is to introduce skeletal semantics, a software framework for specifying and analysing programming languages, and provide a mathematical foundation for it. To this end, we will first introduce SKI calculus as an example of a target programming language and we will show how skeletal semantics can be used to specify it. In a second part, we will motivate our mathematical setting by introducing initial algebra semantics and Lawvere theories, before studying virtual double theories. They are a virtual-double-categorical extension of the latter, allowing for the interpretation of some morphisms as relations. Finally, we show that a skeletal specification (in particular the one of the SKI calculus) may be interpreted as a presentation of a virtual double theory, so that its category of models provides the intended language.