Inductive definitions, semantics and abstract interpretation

Patrick Cousot, Radhia Cousot

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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 GSOS, 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 GSOS by abstract interpretation.

Original languageEnglish (US)
Title of host publicationConference Record of the Annual ACM Symposium on Principles of Programming Languages
Editors Anon
PublisherPubl by ACM
Pages83-94
Number of pages12
ISBN (Print)0897914538
StatePublished - 1992
Event19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Albuquerque, NM, USA
Duration: Jan 19 1992Jan 22 1992

Other

Other19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
CityAlbuquerque, NM, USA
Period1/19/921/22/92

Fingerprint

Semantics
Specifications
Computer science

ASJC Scopus subject areas

  • Software

Cite this

Cousot, P., & Cousot, R. (1992). Inductive definitions, semantics and abstract interpretation. In Anon (Ed.), Conference Record of the Annual ACM Symposium on Principles of Programming Languages (pp. 83-94). Publ by ACM.

Inductive definitions, semantics and abstract interpretation. / Cousot, Patrick; Cousot, Radhia.

Conference Record of the Annual ACM Symposium on Principles of Programming Languages. ed. / Anon. Publ by ACM, 1992. p. 83-94.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Cousot, P & Cousot, R 1992, Inductive definitions, semantics and abstract interpretation. in Anon (ed.), Conference Record of the Annual ACM Symposium on Principles of Programming Languages. Publ by ACM, pp. 83-94, 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albuquerque, NM, USA, 1/19/92.
Cousot P, Cousot R. Inductive definitions, semantics and abstract interpretation. In Anon, editor, Conference Record of the Annual ACM Symposium on Principles of Programming Languages. Publ by ACM. 1992. p. 83-94
Cousot, Patrick ; Cousot, Radhia. / Inductive definitions, semantics and abstract interpretation. Conference Record of the Annual ACM Symposium on Principles of Programming Languages. editor / Anon. Publ by ACM, 1992. pp. 83-94
@inproceedings{f6058b4d993f44d7929686fd1bcebe2f,
title = "Inductive definitions, semantics and abstract interpretation",
abstract = "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.",
author = "Patrick Cousot and Radhia Cousot",
year = "1992",
language = "English (US)",
isbn = "0897914538",
pages = "83--94",
editor = "Anon",
booktitle = "Conference Record of the Annual ACM Symposium on Principles of Programming Languages",
publisher = "Publ by ACM",

}

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

SP - 83

EP - 94

BT - Conference Record of the Annual ACM Symposium on Principles of Programming Languages

A2 - Anon, null

PB - Publ by ACM

ER -