Wow, I just discovered this thread where Thorsten Altenkirch declares small-step operational semantics a "historical mistake." Sometimes I forget how specific the research culture I'm a part of is; given how often I use small-step semantics and abstract machines, I just assume that's what everyone does. But there are many people who consider big-step semantics to be more "natural." (Whatever that means.)
What confuses me about the popularity of big-step semantics in the typed functional language community is that Matthias's approach to proving type soundness via subject reduction in a small-step operational semantics is by now the de facto standard technique.
Anyway, I honestly have no idea how you'd reason about non-trivial language features like continuations with a big-step semantics.
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment