 |
 |
 |
 |
 |
 |
 |
 |
Specification and Abstraction of Semantics.
In A tribute workshop and festival to honor Professor Dr. Neil D. Jones 25-26 August, 2007, Lille Auditorium, Datalogisk Institut, Københavns Universitet, Universitetsparken 1, København, Denmark.
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 lambda-calculus.
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.
\bibitem{CousotCousot07-NDJones}
P. Cousot & R. Cousot.
\newblock Specification and Abstraction of Semantics.
\newblock In \emph{A tribute workshop and festival to honor Professor Dr.\
Neil D.\ Jones}, Lille Auditorium, Datalogisk Institut, K{\o}benhavns
Universitet, Universitetsparken 1, K{\o}benhavn, Denmark, 25--26 August
2007.
@collection{CousotCousot07-NDJones,
author = {P{.} Cousot and R{.} Cousot},
title = {Specification and Abstraction of Semantics},
booktitle = {A tribute workshop and festival to honor Professor Dr.\
Neil D.\ Jones},
address = {25--26 August, 2007},
series = {Lille Auditorium, Datalogisk Institut},
publisher = {K{\o}benhavns Universitet, Universitetsparken 1,
K{\o}benhavn, Denmark},
month = aug # " 25--26",
year = 2007,
}