Coinductive big-step operational semantics

DOI10.1016/j.ic.2007.12.004zbMath1165.68044OpenAlexW1982866418MaRDI QIDQ1012129

Xavier Leroy, Hervé Grall

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

zbMATH Keywords

operational semanticsreduction semanticscoinductiontype soundnessbig-step semanticsnatural semanticssmall-step semanticscompiler correctnessmechanized proofsthe Coq proof assistant

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

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

• Coq
• CompCert

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