Bi-inductive structural semantics

Patrick Cousot, Radhia Cousot

Research output: Contribution to journalArticlepeer-review


We propose a simple order-theoretic generalization, possibly nonmonotone, of settheoretic inductive definitions. This generalization covers inductive, co-inductive and bi-inductive definitions and is preserved by abstraction. This allows structural operational semantics to describe simultaneously the finite/terminating and infinite/diverging behaviors of programs. This is illustrated on grammars and the structural bifinitary small/big-step trace/relational/operational semantics of the call-by-value λ-calculus (for which co-induction is shown to be inadequate).

Original languageEnglish (US)
Pages (from-to)258-283
Number of pages26
JournalInformation and Computation
Issue number2
StatePublished - Feb 2009


  • Bi-inductive definition
  • Big-step semantics
  • Co-inductive definition
  • Divergence semantics
  • Fixpoint definition
  • Grammar
  • Inductive definition
  • Nonmonotone definition
  • Relational semantics
  • SOS
  • Small-step semantics
  • Structural operational semantics
  • Trace semantics

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Information Systems
  • Computer Science Applications
  • Computational Theory and Mathematics


Dive into the research topics of 'Bi-inductive structural semantics'. Together they form a unique fingerprint.

Cite this