Flag-based big-step semantics

DOI10.1016/J.JLAMP.2016.05.001MaRDI QIDQ516041zbMATH OpenOpenAlexFDO

Authors Casper Bach Poulsen, Peter D. Mosses

Publication date 20 March 2017

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1605.02935, https://cronfa.swan.ac.uk/Record/cronfa28828/Download/0028828-10062016153907.pdf

zbMATH Keywords

coinductionstructural operational semanticsSOSbig-step semanticsnatural semanticssmall-step semantics

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Abstract: Structural operational semantic specifications come in different styles: small-step and big-step. A problem with the big-step style is that specifying divergence and abrupt termination gives rise to annoying duplication. We present a novel approach to representing divergence and abrupt termination in big-step semantics using status flags. This avoids the duplication problem, and uses fewer rules and premises for representing divergence than previous approaches in the literature.

Recommendations

• Pretty-big-step semantics
• Deriving Pretty-Big-Step Semantics from Small-Step Semantics
• Big-step operational semantics revisited
• scientific article; zbMATH DE number 1231612
• scientific article; zbMATH DE number 1951197

Cites work

• scientific article; zbMATH DE number 1670486 (Why is no real title available?)
• scientific article; zbMATH DE number 4035108 (Why is no real title available?)
• scientific article; zbMATH DE number 3495581 (Why is no real title available?)
• scientific article; zbMATH DE number 1531624 (Why is no real title available?)
• scientific article; zbMATH DE number 7362470 (Why is no real title available?)
• A Brief Overview of Agda – A Functional Language with Dependent Types
• A structural approach to operational semantics
• A syntactic approach to type soundness
• Calculating correct compilers
• Coinductive big-step operational semantics
• Concrete semantics. With Isabelle/HOL
• Deriving Pretty-Big-Step Semantics from Small-Step Semantics
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Generating specialized interpreters for modular structural operational semantics
• Implicit propagation in structural operational semantics
• Introduction to bisimulation and coinduction
• Modular bisimulation theory for computations and values
• Modular structural operational semantics
• Notions of computation and monads
• On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion
• On the proof theory of Coquand's calculus of constructions
• Operational semantics using the partiality monad
• Pretty-big-step semantics
• Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction
• The calculus of constructions
• The coinductive resumption monad
• The power of parameterization in coinductive proof
• Trace-Based Coinductive Operational Semantics for While
• Types and programing languages
• What is the meaning of these constant interruptions?

Cited in

(5)

• Soundness conditions for big-step semantics
• Pretty-big-step semantics
• Characteristic formulae for liveness properties of non-terminating CakeML programs
• Big-step operational semantics revisited
• Generalizing inference systems by coaxioms

Describes a project that uses

Uses Software

• MiniAgda
• Paco
• Agda

This page was built for publication: Flag-based big-step semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q516041)