Coinductive big-step operational semantics
From MaRDI portal
Publication:1012129
DOI10.1016/j.ic.2007.12.004zbMath1165.68044MaRDI 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 semantics; reduction semantics; coinduction; type soundness; big-step semantics; natural semantics; small-step semantics; compiler correctness; mechanized proofs; the Coq proof assistant
68Q55: Semantics in the theory of computing
Related Items
Structural operational semantics through context-dependent behaviour, Transfinite semantics in the form of greatest fixpoint, Mechanized semantics for the clight subset of the C language, A formally verified compiler back-end, Probabilistic operational semantics for the lambda calculus, Idealized coinductive type systems for imperative object-oriented programs, Trace-Based Coinductive Operational Semantics for While, Translation Correctness for First-Order Object-Oriented Pattern Matching
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
