Bi-inductive Structural Semantics. (Extended Abstract)

Patrick Cousot, Radhia Cousot

Research output: Contribution to journalArticlepeer-review


We propose a simple order-theoretic generalization of set-theoretic inductive definitions. This generalization covers inductive, co-inductive and bi-inductive definitions and is preserved by abstraction. This allows the structural operational semantics to describe simultaneously the finite/terminating and infinite/diverging behaviors of programs. This is illustrated on the structural bifinitary small/big-step trace/relational/operational semantics of the call-by-value λ-calculus.

Original languageEnglish (US)
Pages (from-to)29-44
Number of pages16
JournalElectronic Notes in Theoretical Computer Science
Issue number1 SPEC. ISS.
StatePublished - Oct 24 2007


  • SOS
  • abstraction
  • bi-inductive definition
  • big-step semantics
  • co-inductive definition
  • divergence semantics
  • fixpoint definition
  • inductive definition
  • relational semantics
  • small-step semantics
  • structural operational semantics
  • trace semantics

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Bi-inductive Structural Semantics. (Extended Abstract)'. Together they form a unique fingerprint.

Cite this