Классика computer science: "The spineless tagless G-machine, naturally"
Spineless Tagless G-machine (STG) -- абстрактная машина, лежащая в основе легендарного компилятора Glasgow Haskell Compiler (GHC). В оригинале использовали Natural Semantics для ленивых вычислений Джона Лончбери как основу для формального вывода и доказательства корректности STM. Но затем Джон Маунтджой разработал расширенную семантику лямбда-исчислений, из которой удалось формально вывести полноценную STG-машину, что послужило доказательством её корректности по отношению к эталонной семантике Лончбери.