Skeletal Semantics


This page regroups information related to the thesis "Skeletal Semantics Transformations" by Guillaume Ambal. Here are the short and long versions.

The appendices are available individually: the functional correspondence example on IMP, the big-step to small-step transformation phases on IMP, the paper proof of the transformation, and the derivation of the two abstract machines.

The implementation files are available on the Inria Gitlab for the first and second part of the thesis.