P. Cousot & R. Cousot, Bi-inductive Structural Semantics

Patrick Cousot & Radhia Cousot.
Bi-inductive Structural Semantics.
In Information and computation 207(2):258—283, February 2009.
Full version of the SOS'07 article.
Paper:
- PDF (860 Kb)
Abstract:
We propose a simple order-theoretic generalization, possibly non monotone, of set-theoretic 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 lambda-calculus (for which co-induction is shown to be inadequate).
Keywords:
Fixpoint definition, inductive definition, co-inductive definition, bi-inductive definition, structural operational semantics, SOS, trace semantics, relational semantics, small-step semantics, big-step semantics, divergence semantics, abstraction.

Bibliographic reference:

\bibitem{CousotCousot08-IC}
P. Cousot & R. Cousot.
\newblock Bi-inductive Structural Semantics.
\newblock In \emph{Information and Computation}, 207(2)2:258--283, February 2009.

@article{CousotCousot08-IC,
   author =    {P{.} Cousot and R{.} Cousot},
   title =     {Bi-inductive Structural Semantics},
   journal =   {Information and Computation},
   volume =    {207},
   number =    {2},
   year =      2009,
   pages =     {258--283},
}

copyright notice, Elsevier copyright
Last modified: Tuesday, 29-Sep-2015 18:05:25 EDT