Reduction Semantics and How to Read Them
The semantics of a programming language is often given by defining a set of simplification rules (e.g., 1+1 simplifies to 2, (car (cons 1 '()) simplifies to 1) and a set of contexts where these simplifications are allowed to occur (e.g., in the test position of an if, but not in the branches). These steps are then chained together into reduction sequences that start from an arbitrary program in the language and end with the program’s final result (or never end, if the program runs forever).
This style of semantics is able to describe a wide range of languages, from simple ones that are little more than arithmetic to sophisticated ones with fancy forms of control flow. Critical to the ease and concision is the notion of an evaluation context which, roughly speaking, captures where the simplification steps are allowed to occur via productions in a grammar.
In this talk, I will give an overview of the way these semantics are defined and a sense of the commonly used patterns. We will see how different orders of evaluation, underspecification of the language, and complex control flow (e.g., exceptions and continuations) are all just a matter of using the basic tools in creative ways. By the end of the talk, you should be able to get a basic understanding of the semantics of a language in paper by studying its reduction relation’s rules and working through a few examples.
Mon 24 AugDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:30 | |||
14:00 45mTalk | Writing Makes the Researcher: The First Audience Is You PLMW @ ICFP Benjamin Delaware Purdue University | ||
14:45 45mTalk | Reduction Semantics and How to Read Them PLMW @ ICFP Robert Bruce Findler Northwestern University | ||