Bi-inductive Structural Semantics. (Extended Abstract)

Patrick Cousot; Radhia Cousot

doi:10.1016/j.entcs.2007.08.015

Bi-inductive Structural Semantics. (Extended Abstract)

Patrick Cousot, Radhia Cousot

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

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 language	English (US)
Pages (from-to)	29-44
Number of pages	16
Journal	Electronic Notes in Theoretical Computer Science
Volume	192
Issue number	1 SPEC. ISS.
DOIs	https://doi.org/10.1016/j.entcs.2007.08.015
State	Published - Oct 24 2007

Keywords

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

Access to Document

10.1016/j.entcs.2007.08.015

Cite this

@article{65de30cdded24f55b9a2dd4efecf5356,

title = "Bi-inductive Structural Semantics. (Extended Abstract)",

abstract = "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.",

keywords = "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",

author = "Patrick Cousot and Radhia Cousot",

year = "2007",

month = oct,

day = "24",

doi = "10.1016/j.entcs.2007.08.015",

language = "English (US)",

volume = "192",

pages = "29--44",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

number = "1 SPEC. ISS.",

}

TY - JOUR

T1 - Bi-inductive Structural Semantics. (Extended Abstract)

AU - Cousot, Patrick

AU - Cousot, Radhia

PY - 2007/10/24

Y1 - 2007/10/24

N2 - 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.

AB - 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.

KW - SOS

KW - abstraction

KW - bi-inductive definition

KW - big-step semantics

KW - co-inductive definition

KW - divergence semantics

KW - fixpoint definition

KW - inductive definition

KW - relational semantics

KW - small-step semantics

KW - structural operational semantics

KW - trace semantics

UR - http://www.scopus.com/inward/record.url?scp=35349005107&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=35349005107&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2007.08.015

DO - 10.1016/j.entcs.2007.08.015

M3 - Article

AN - SCOPUS:35349005107

SN - 1571-0661

VL - 192

SP - 29

EP - 44

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 1 SPEC. ISS.

ER -

Bi-inductive Structural Semantics. (Extended Abstract)

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this