Big Steps in Higher-Order Mathematical Operational Semantics
Small-step and big-step operational semantics are two fundamental styles of structural operational semantics (SOS), extensively used in practice. The former one is more fine-grained and is usually regarded as primitive, as it only defines a one-step reduction relation between a given program and its direct descendant under an ambient evaluation strategy. The latter one implements, in a self-contained manner, such a strategy directly by relating a program to the net result of the evaluation process. The agreement between these two styles of semantics is one of the key pillars in operational reasoning on programs; however, such agreement is typically proven from scratch every time on a case-by-case basis. A general, abstract mathematical argument behind this agreement is up till now missing. We cope with this issue within the framework of higher-order mathematical operational semantics by providing an abstract categorical notion of big-step SOS, complementing the existing notion of abstract higher-order GSOS. Moreover, we introduce a general construction for deriving the former from the latter, and prove an abstract equivalence result between the two.
Mon 13 OctDisplayed time zone: Perth change
16:00 - 17:40 | SemanticsJFP First Papers / ICFP Papers at Orchid West Chair(s): Henning Urbat Friedrich-Alexander University Erlangen-Nürnberg | ||
16:00 25mPaper | A contextual formalization of structural coinduction JFP First Papers DOI | ||
16:25 25mPaper | A practical formalization of monadic equational reasoning in dependent-type theory JFP First Papers Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Japan, Jacques Garrigue Nagoya University, Takafumi Saikawa Nagoya University DOI File Attached | ||
16:50 25mTalk | Almost Fair Simulations ICFP Papers Arthur Correnson CISPA Helmholtz Center for Information Security, Iona Kuhn Saarland University, Bernd Finkbeiner CISPA Helmholtz Center for Information Security DOI | ||
17:15 25mTalk | Big Steps in Higher-Order Mathematical Operational Semantics ICFP Papers Sergey Goncharov University of Birmingham, Pouya Partow Birmingham University, Stelios Tsampas University of Southern Denmark DOI | ||