Coinductive big-step operational semantics
From MaRDI portal
Publication:1012129
DOI10.1016/J.IC.2007.12.004zbMATH Open1165.68044OpenAlexW1982866418MaRDI QIDQ1012129FDOQ1012129
Authors: 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
Recommendations
- Programming Languages and Systems
- Trace-Based Coinductive Operational Semantics for While
- Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction
- Bi-inductive structural semantics
- Bi-inductive structural semantics (extended abstract)
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: programming a compiler with a proof assistant
- 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 (28)
- Soundness conditions for big-step semantics
- 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?)
- Programming Languages and Systems
- Characteristic formulae for liveness properties of non-terminating CakeML programs
- Modular relaxed dependencies in weak memory concurrency
- Translation Correctness for First-Order Object-Oriented Pattern Matching
- Generalizing inference systems by coaxioms
- Squeezing streams and composition of self-stabilizing algorithms
- Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction
- Non-well-founded deduction for induction and coinduction
- Integrating induction and coinduction via closure operators and proof cycles
- Probabilistic operational semantics for the lambda calculus
- Trace-Based Coinductive Operational Semantics for While
- 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
- Bi-inductive structural semantics (extended abstract)
- Formal verifications of call-by-need and call-by-name evaluations with mutual recursion
- Idealized coinductive type systems for imperative object-oriented programs
- Title not available (Why is that?)
- Flag-based big-step semantics
Uses Software
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)
