With my collaborators Arthur Charguéraud, Adam Chlipala and Andres Erbsen, we came up with a new style of programming language semantics that we find works much better in the presence of undefined behavior and nondeterminism than traditional bigstep and smallstep operational semantics do. We called it omnisemantics because one derivation talks about all (omni) possible nondeterministic executions at once.

Yesterday, I gave a talk about it at the NEPLS workshop, and because I enjoyed giving that talk so much, I decided to take some screenshots of my slides and turn the talk into a blog post.

If you saw the talk, or have already heard about omnisemantics and you want to learn (almost) everything we have to say about it, I’d recommend reading the preprint of our paper that you can find here. On the other hand, if you prefer just a quick intro, at the level of detail of a workshop talk, this blog post might be for you!

While working with Coq’s JSON extraction, Thomas and I were quite puzzled when the AST generated by extraction did not match the original Gallina syntax: Some functions were silently unfolded, even though we never told Coq to do so. With Tej’s help, we figured out what’s going on, and after some thinking, it all started to make sense.

This is (roughly) the transcript of a 5 minute lightning talk I gave at the DeepSpec workshop at PLDI’18.