ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Mon 8 Apr 2019 15:30 - 16:00 at SUN II - Language Design Chair(s): Atsushi Igarashi

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 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 16:00
Language DesignESOP at SUN II
Chair(s): Atsushi Igarashi Kyoto University, Japan
14:00
30m
Talk
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
30m
Talk
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
30m
Talk
Counters in Kappa: Semantics, Simulation, and Static Analysis
ESOP
Pierre Boutillier , Ioana Cristescu INRIA, France, Jerome Feret INRIA Paris
Link to publication
15:30
30m
Talk
One Step at a Time
ESOP
Kathleen Fisher Tufts University, Ferdinand Vesely Swansea University
Link to publication