TY - GEN
T1 - Inductive definitions, semantics and abstract interpretation
AU - Cousot, Patrick
AU - Cousot, Radhia
PY - 1992
Y1 - 1992
N2 - We introduce and illustrate a specification method combining rule-based inductive definitions, well-founded induction principles, fixed-point theory and abstract interpretation for general use in computer science. Finite as well as infinite objects can be specified, at various levels of details related by abstraction. General proof principles are applicable to prove properties of the specified objects. The specification method is illustrated by introducing G∞SOS, a structured operational semantics generalizing Plotkin's structured operational semantics (SOS) so as to describe the finite, as well as the infinite behaviors of programs in a uniform way and by constructively deriving inductive presentations of the other (relational, denotational, predicate transformers, ...) semantics from G∞SOS by abstract interpretation.
AB - We introduce and illustrate a specification method combining rule-based inductive definitions, well-founded induction principles, fixed-point theory and abstract interpretation for general use in computer science. Finite as well as infinite objects can be specified, at various levels of details related by abstraction. General proof principles are applicable to prove properties of the specified objects. The specification method is illustrated by introducing G∞SOS, a structured operational semantics generalizing Plotkin's structured operational semantics (SOS) so as to describe the finite, as well as the infinite behaviors of programs in a uniform way and by constructively deriving inductive presentations of the other (relational, denotational, predicate transformers, ...) semantics from G∞SOS by abstract interpretation.
UR - http://www.scopus.com/inward/record.url?scp=0026992713&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0026992713&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:0026992713
SN - 0897914538
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 83
EP - 94
BT - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
A2 - Anon, null
PB - Publ by ACM
T2 - 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Y2 - 19 January 1992 through 22 January 1992
ER -