Coinductive big-step operational semantics
From MaRDI portal
Publication:1012129
DOI10.1016/J.IC.2007.12.004zbMATH Open1165.68044OpenAlexW1982866418MaRDI QIDQ1012129FDOQ1012129
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
coinductionoperational semanticstype soundnessbig-step semanticsnatural semanticssmall-step semanticscompiler correctnessreduction semanticsmechanized proofsthe Coq proof assistant
Cites Work
- A structural approach to operational semantics
- A lattice-theoretical fixpoint theorem and its applications
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A syntactic approach to type soundness
- Title not available (Why is that?)
- Recursive subtyping revealed
- The Mechanical Evaluation of Expressions
- Title not available (Why is that?)
- Infinite \(\lambda\)-calculus and types
- Infinitary lambda calculus
- Formal certification of a compiler back-end or
- A co-induction principle for recursively defined domains
- Typed Lambda Calculi and Applications
- Title not available (Why is that?)
- The categorical abstract machine
- Functional runtime systems within the lambda-sigma calculus
- Co-induction in relational semantics
- Making a fast curry: push/enter vs. eval/apply for higher-order languages
- Bi-inductive structural semantics (extended abstract)
- Coinductive Logic Programming
Cited In (25)
- Transfinite semantics in the form of greatest fixpoint
- A formally verified compiler back-end
- Flexible coinductive logic programming
- Title not available (Why is that?)
- Structural operational semantics through context-dependent behaviour
- Proving correctness of a compiler using step-indexed logical relations
- Checking equivalence of corecursive streams: an inductive procedure
- Title not available (Why is that?)
- Characteristic formulae for liveness properties of non-terminating CakeML programs
- Translation Correctness for First-Order Object-Oriented Pattern Matching
- Squeezing streams and composition of self-stabilizing algorithms
- Non-well-founded deduction for induction and coinduction
- Integrating induction and coinduction via closure operators and proof cycles
- Soundness Conditions for Big-Step Semantics
- Probabilistic operational semantics for the lambda calculus
- Trace-Based Coinductive Operational Semantics for While
- Generalizing Inference Systems by Coaxioms
- Inductive and coinductive predicate liftings for effectful programs
- A list-machine benchmark for mechanized metatheory
- Mechanized semantics for the clight subset of the C language
- Formal verifications of call-by-need and call-by-name evaluations with mutual recursion
- Modular Relaxed Dependencies in Weak Memory Concurrency
- Idealized coinductive type systems for imperative object-oriented programs
- Title not available (Why is that?)
- Flag-based big-step semantics
Uses Software
Recommendations
This page was built for publication: Coinductive big-step operational semantics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1012129)
