Coinductive big-step operational semantics
From MaRDI portal
Publication:1012129
DOI10.1016/j.ic.2007.12.004zbMath1165.68044OpenAlexW1982866418MaRDI QIDQ1012129
Publication date: 14 April 2009
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2007.12.004
operational semanticsreduction semanticscoinductiontype soundnessbig-step semanticsnatural semanticssmall-step semanticscompiler correctnessmechanized proofsthe Coq proof assistant
Related Items
Soundness Conditions for Big-Step Semantics ⋮ Modular Relaxed Dependencies in Weak Memory Concurrency ⋮ Transfinite semantics in the form of greatest fixpoint ⋮ Probabilistic operational semantics for the lambda calculus ⋮ Trace-Based Coinductive Operational Semantics for While ⋮ Mechanized semantics for the clight subset of the C language ⋮ A formally verified compiler back-end ⋮ Translation Correctness for First-Order Object-Oriented Pattern Matching ⋮ Squeezing streams and composition of self-stabilizing algorithms ⋮ A list-machine benchmark for mechanized metatheory ⋮ Structural operational semantics through context-dependent behaviour ⋮ Generalizing Inference Systems by Coaxioms ⋮ Unnamed Item ⋮ Flexible coinductive logic programming ⋮ Characteristic formulae for liveness properties of non-terminating CakeML programs ⋮ Idealized coinductive type systems for imperative object-oriented programs ⋮ Proving correctness of a compiler using step-indexed logical relations ⋮ Flag-based big-step semantics ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Non-well-founded deduction for induction and coinduction ⋮ Integrating induction and coinduction via closure operators and proof cycles
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- The categorical abstract machine
- Co-induction in relational semantics
- Infinite \(\lambda\)-calculus and types
- A co-induction principle for recursively defined domains
- A syntactic approach to type soundness
- Infinitary lambda calculus
- A structural approach to operational semantics
- A lattice-theoretical fixpoint theorem and its applications
- Bi-inductive Structural Semantics
- Functional runtime systems within the lambda-sigma calculus
- Recursive subtyping revealed
- Formal certification of a compiler back-end or
- Coinductive Logic Programming
- Making a fast curry: push/enter vs. eval/apply for higher-order languages
- Typed Lambda Calculi and Applications
- The Mechanical Evaluation of Expressions
