Coinductive big-step operational semantics
From MaRDI portal
Publication:1012129
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)
Cites work
- scientific article; zbMATH DE number 4035108 (Why is no real title available?)
- scientific article; zbMATH DE number 3631912 (Why is no real title available?)
- scientific article; zbMATH DE number 1241702 (Why is no real title available?)
- A co-induction principle for recursively defined domains
- A lattice-theoretical fixpoint theorem and its applications
- A structural approach to operational semantics
- A syntactic approach to type soundness
- Bi-inductive structural semantics (extended abstract)
- Co-induction in relational semantics
- Coinductive Logic Programming
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Functional runtime systems within the lambda-sigma calculus
- Infinitary lambda calculus
- Infinite \(\lambda\)-calculus and types
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Making a fast curry: push/enter vs. eval/apply for higher-order languages
- Recursive subtyping revealed
- The Mechanical Evaluation of Expressions
- The categorical abstract machine
- Typed Lambda Calculi and Applications
Cited in
(28)- Checking equivalence of corecursive streams: an inductive procedure
- Trace-Based Coinductive Operational Semantics for While
- Soundness conditions for big-step semantics
- Inductive and coinductive predicate liftings for effectful programs
- Characteristic formulae for liveness properties of non-terminating CakeML programs
- Translation Correctness for First-Order Object-Oriented Pattern Matching
- A formally verified compiler back-end
- Non-well-founded deduction for induction and coinduction
- A list-machine benchmark for mechanized metatheory
- Probabilistic operational semantics for the lambda calculus
- Flexible coinductive logic programming
- Resumptions, weak bisimilarity and big-step semantics for While with interactive I/O: an exercise in mixed induction-coinduction
- scientific article; zbMATH DE number 7471662 (Why is no real title available?)
- Formal verifications of call-by-need and call-by-name evaluations with mutual recursion
- Idealized coinductive type systems for imperative object-oriented programs
- Transfinite semantics in the form of greatest fixpoint
- Structural operational semantics through context-dependent behaviour
- scientific article; zbMATH DE number 7199590 (Why is no real title available?)
- scientific article; zbMATH DE number 7037626 (Why is no real title available?)
- Modular relaxed dependencies in weak memory concurrency
- Integrating induction and coinduction via closure operators and proof cycles
- Proving correctness of a compiler using step-indexed logical relations
- Flag-based big-step semantics
- Generalizing inference systems by coaxioms
- Bi-inductive structural semantics (extended abstract)
- Squeezing streams and composition of self-stabilizing algorithms
- Mechanized semantics for the clight subset of the C language
- Programming Languages and Systems
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)
