Интересная штука.

[thesz]

K: A Rewriting-Based Framework for Computations.

Чем интересна - описывается семантика программ через переписывание термов (term rewriting). И у меня есть воздушное такое ощущение, что можно показывать компиляцию программ из одного языка в другой следующим образом: compile_triple(S, TA, Q) -> TB iff execute_A(S, TA, Q) = execute_B(predicate_transform_AB(S), TB, predicate_transform_AB(Q)).

Вот ещё на закуску. Компиляция функционального языка в машинный код (с распределением регистров даже) через переписывание термов.