Big-step and small-step are two popular flavors of operational semantics. Big-step is often seen as a more natural transcription of informal descriptions, as well as being more convenient for some applications such as interpreter generation or optimization verification. Small-step allows reasoning about non-terminating computations, concurrency and interactions. It is also generally preferred for reasoning about type systems. Instead of having to manually specify equivalent semantics in both styles for different applications, it would be useful to choose one and derive the other in a systematic or, preferably, automatic way.
Transformations of small-step semantics into big-step have been investigated in various forms by Danvy and others. However, it appears that a corresponding transformation from big-step to small-step semantics has not had the same attention. We present a fully automated transformation that maps big-step evaluators written in direct style to their small-step counterparts. Many of the steps in the transformation, which include CPS-conversion, defunctionalization, and various continuation manipulations, mirror those used by Danvy and his co-authors. For many standard languages, including those with either call-by-value or call-by-need and those with state, the transformation produces small-step semantics that are close in style to handwritten ones. We evaluate the applicability and correctness of the approach on 20 languages with a range of features.
Mon 8 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 16:00 | |||
14:00 30mTalk | Codata in Action ESOP Paul Downen University of Oregon, USA, Zachary Sullivan , Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft, UK Link to publication | ||
14:30 30mTalk | Composing bidirectional programs monadically ESOP Li-yao Xia University of Pennsylvania, Dominic Orchard University of Kent, UK, Meng Wang University of Bristol, UK Link to publication | ||
15:00 30mTalk | Counters in Kappa: Semantics, Simulation, and Static Analysis ESOP Link to publication | ||
15:30 30mTalk | One Step at a Time ESOP Link to publication |