More Web Proxy on the site http://driver.im/

article

Bi-inductive structural semantics

Authors:

Patrick Cousot,

Radhia CousotAuthors Info & Claims

Information and Computation, Volume 207, Issue 2

Pages 258 - 283

https://doi.org/10.1016/j.ic.2008.03.025

Published: 01 February 2009 Publication History

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 @l-calculus (for which co-induction is shown to be inadequate).

References

[1]

Abramsky, S., Semantics of interaction: an introduction to game semantics. In: Pitts, A.M., Dybjer, P. (Eds.), Semantics and Logics of Computation, Cambridge University Press, Cambridge, UK. pp. 1-32.

[2]

Aczel, P., An introduction to inductive definitions. In: Barwise, J. (Ed.), Studies in Logic and the Foundations of Mathematics, vol. 90. Elsevier Science Publishers BV, Amsterdam, The Netherlands. pp. 739-782.

[3]

I. Attali, J. Chazarain, S. Gilette, Incremental evaluation of natural semantics specifications, in: M. Bruynooghe, M. Wirsing, (Eds.), Proceedings of the Fourth International Symposium on Programming Language Implementation and Logic Programming, PLILP'92, Leuven, Belgium, 26--28 August 1992, Lecture Notes in Computer Science, vol. 631, Springer, Berlin, Germany, 1992, pp. 87--99.

Digital Library

[4]

Chomsky, N. and Schützenberger, M.P., The algebraic theory of context-free languages. In: Bradford, P., Hirschberg, D. (Eds.), Computer Programming and Formal Systems, North Holland Pub. Co., Amsterdam, The Netherlands. pp. 118-161.

[5]

P. Cousot, Types as abstract interpretations, invited paper, in: Conference Record of the Twentyfourth Annual ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages, Paris, France, ACM Press, New York, USA, January 1997, pp. 316--331.

Digital Library

[6]

Cousot, P., Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science. v277 i1--2. 47-103.

Digital Library

[7]

Cousot, P. and Cousot, R., Constructive versions of Tarski's fixed point theorems. Pacific Journal of Mathematics. v82 i1. 43-57.

[8]

P. Cousot, R. Cousot, Systematic design of program analysis frameworks, in: Conference Record of the Sixth Annual ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages, San Antonio, Texas, ACM Press, New York, USA, 1979, pp. 269--282.

Digital Library

[9]

Cousot, P. and Cousot, R., Abstract interpretation frameworks. Journal of Logic and Computation. v2 i4. 511-547.

[10]

P. Cousot, R. Cousot, Inductive definitions, semantics and abstract interpretation, in: Conference Record of the Ninthteenth Annual ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, United States, ACM Press, New York, USA, 1992, pp. 83--94.

Digital Library

[11]

P. Cousot, R. Cousot, Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form, invited paper, in: P. Wolper, (Ed.), Proceedings of the Seventh International Conference on Computer Aided Verification, CAV'95, Liège, Belgium, Lecture Notes in Computer Science, vol. 939, Springer, Berlin, Germany, 3--5 July 1995, pp. 293--308.

Digital Library

[12]

Davey, B.A. and Priestley, H.A., Introduction to Lattices and Order. 2002. second ed. Cambridge University Press, Cambridge, UK.

[13]

Th. Despeyroux, TYPOL: A Formalism to Implement Natural Semantics, Technical Report RT--0094, INRIA Sophia Antipolis, March 1988.

[14]

Ginsburg, S. and Rice, G., Two families of languages related to ALGOL. Journal of the Association for Computing Machinery. v9. 350-371.

Digital Library

[15]

Hoare, C.A.R., An axiomatic basis for computer programming. Communications of the Association for Computing Machinery. v12 i10. 576-580.

Digital Library

[16]

Jacobs, B. and Rutten, J., A tutorial on (co)algebras and (co)induction. EATCS Bulletin. v62. 222-269.

[17]

Kahn, G., Natural semantics. In: Fuchi, K., Nivat, M. (Eds.), Programming of Future Generation Computers, Elsevier Science Publishers BV, Amsterdam, The Netherlands. pp. 237-258.

Digital Library

[18]

Kanamori, A., The mathematical import of Zermelo's well-ordering theorem. Bulletin of Symbolic Logic. v3. 281-311.

[19]

Klin, B., Adding recursive constructs to bialgebraic semantics. Journal of Logic and Algebraic Programming. v60--61. 259-286.

[20]

Klin, B., Bialgebraic methods in structural operational semantics. Electronic Notes in Theoretical Computer Science. v175 i1. 33-43.

Digital Library

[21]

Lassez, J.-L., Nguyen, V.L. and Sonenberg, L., Fixed point theorems and semantics: a folk tale. Information Processing Letters. v14 i3. 112-116.

[22]

X. Leroy, Coinductive big-step operational semantics, in: P. Sestoft, (Ed.), Proceedings of the Fifteenth European Symposium on Programming Languages and Systems, ESOP'2006, Vienna, Austria, Lecture Notes in Computer Science, vol. 3924, Springer, Berlin, Germany, 27--28 March 2006, pp. 54--68.

Digital Library

[23]

Milner, R., Operational and algebraic semantics of concurrent processes. In: van Leeuwen, J. (Ed.), Handbook of Theoretical Computer Science, vol. B. Elsevier Science Publishers BV, Amsterdam, The Netherlands. pp. 1201-1242.

Digital Library

[24]

Mosses, P.D., Denotational semantics. In: van Leeuwen, J. (Ed.), Handbook of Theoretical Computer Science, vol. B. Elsevier Science Publishers BV, Amsterdam, The Netherlands. pp. 575-631.

Digital Library

[25]

A. Mycroft, The theory and practice of transforming call-by-need into call-by-value, in: B. Robinet, (Ed.), Proceedings of the Fourth International Symposium on Programming, Paris, France, 22--24 April 1980, Lecture Notes in Computer Science, vol. 83, Springer, Berlin, Germany, 1980, pp. 270--281.

Digital Library

[26]

Nivat, M., Sur les ensembles de mots infinis engendrés par une grammaire algébrique. Informatique Théorique et Applications. v12 i3. 259-278.

[27]

D. Pataria, A constructive proof of Tarski's fixed-point theorem for dcpo's, 65th Peripatetic Seminar on Sheaves and Logic, Århus, Denmark, November 1997. Reported by M.H. Escardó in Joins in the frame of nuclei, Applied Categorical Structures, vol. 11, Issue 2, April 2003, pp. 117--124.

[28]

G.D. Plotkin, A Structural Approach to Operational Semantics, Technical Report DAIMI FN--19, Aarhus University, Denmark, September 1981. Reprinted in {30}.

[29]

Plotkin, G.D., The origins of structural operational semantics. Journal of Logic and Algebraic Programming. v60--61. 3-15.

[30]

Plotkin, G.D., A structural approach to operational semantics. Journal of Logic and Algebraic Programming. v60--61. 17-139.

[31]

Schützenberger, M.P., On a theorem of R. Jungen. Proceedings of the American Mathematical Society. v13. 885-889.

[32]

P. Steckler, M. Wand. Selective thunkification, in: B. Le Charlier, (Ed.), Proceedings of the First International Symposium on Static Analysis, SAS'94, Namur, Belgium, 20--22 September 1994, Lecture Notes in Computer Science, vol. 864, Springer, Berlin, Germany, 1994, pp. 162--178.

[33]

Tarski, A., A lattice theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics. v5. 285-310.

[34]

D. Turi, G.D. Plotkin, Towards a mathematical operational semantic, in: G. Winskel, (Ed.), Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS'1997, Warsaw, Poland, 29 June--2 July 1997, IEEE Computer Society Press, Los Alamitos, California, USA, pp. 280--291.

Digital Library

[35]

van Breugel, F., An introduction to metric semantics: operational and denotational models for programming and specification languages. Theoretical Computer Science. v258. 1-98.

Digital Library

Cited By

Cousot P(2019)Syntactic and Semantic Soundness of Structural Dataflow AnalysisStatic Analysis10.1007/978-3-030-32304-2_6(96-117)Online publication date: 8-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-32304-2_6
Ancona DDagnino FZucca E(2017)Reasoning on divergent computations with coaxiomsProceedings of the ACM on Programming Languages10.1145/31339051:OOPSLA(1-26)Online publication date: 12-Oct-2017
https://dl.acm.org/doi/10.1145/3133905
Cousot PCousot RHenzinger TMiller D(2014)Abstract interpretationProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1145/2603088.2603165(1-10)Online publication date: 14-Jul-2014
https://dl.acm.org/doi/10.1145/2603088.2603165
Show More Cited By

Index Terms

Bi-inductive structural semantics
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Formal languages and automata theory
    1. Formalisms
      1. Rewrite systems
    2. Grammars and context-free languages
  2. Semantics and reasoning
    1. Program semantics

Recommendations

Bi-inductive Structural Semantics

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 ...
Coinductive big-step operational semantics

Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We ...
Deriving Pretty-Big-Step Semantics from Small-Step Semantics
Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410

Big-step semantics for languages with abrupt termination and/or divergence suffer from a serious duplication problem, addressed by the novel 'pretty-big-step' style presented by Charguéraud at ESOP'13. Such rules are less concise than corresponding ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Information and Computation

Information and Computation Volume 207, Issue 2

February, 2009

288 pages

ISSN:0890-5401

Issue’s Table of Contents

Copyright © Elsevier Inc. © 2008.

Publisher

Academic Press, Inc.

United States

Publication History

Published: 01 February 2009

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Cousot P(2019)Syntactic and Semantic Soundness of Structural Dataflow AnalysisStatic Analysis10.1007/978-3-030-32304-2_6(96-117)Online publication date: 8-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-32304-2_6
Ancona DDagnino FZucca E(2017)Reasoning on divergent computations with coaxiomsProceedings of the ACM on Programming Languages10.1145/31339051:OOPSLA(1-26)Online publication date: 12-Oct-2017
https://dl.acm.org/doi/10.1145/3133905
Cousot PCousot RHenzinger TMiller D(2014)Abstract interpretationProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1145/2603088.2603165(1-10)Online publication date: 14-Jul-2014
https://dl.acm.org/doi/10.1145/2603088.2603165
Charguéraud A(2013)Pretty-Big-Step semanticsProceedings of the 22nd European conference on Programming Languages and Systems10.1007/978-3-642-37036-6_3(41-60)Online publication date: 16-Mar-2013
https://dl.acm.org/doi/10.1007/978-3-642-37036-6_3
D'Silva VKroening D(2013)Abstraction of SyntaxProceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 773710.1007/978-3-642-35873-9_24(396-413)Online publication date: 20-Jan-2013
https://dl.acm.org/doi/10.1007/978-3-642-35873-9_24
Danielsson N(2012)Operational semantics using the partiality monadACM SIGPLAN Notices10.1145/2398856.236454647:9(127-138)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2398856.2364546
Danielsson NThiemann PFindler R(2012)Operational semantics using the partiality monadProceedings of the 17th ACM SIGPLAN international conference on Functional programming10.1145/2364527.2364546(127-138)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2364527.2364546
Chawdhary AYang H(2010)Metric spaces and termination analysesProceedings of the 8th Asian conference on Programming languages and systems10.5555/1947873.1947889(156-171)Online publication date: 28-Nov-2010
https://dl.acm.org/doi/10.5555/1947873.1947889
Nakata KUustalu T(2010)A hoare logic for the coinductive trace-based big-step semantics of whileProceedings of the 19th European conference on Programming Languages and Systems10.1007/978-3-642-11957-6_26(488-506)Online publication date: 20-Mar-2010
https://dl.acm.org/doi/10.1007/978-3-642-11957-6_26

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents