article

Free access

Remarks on many-sorted equational logic with respect to algebraic implementations

Authors:

Eric van Gestel,

Ivo van HorebeekAuthors Info & Claims

ACM SIGPLAN Notices, Volume 23, Issue 1

Pages 120 - 126

https://doi.org/10.1145/44304.44315

Published: 03 January 1988 Publication History

PDF eReader

References

[1]

ADJ: Goguen, J. A., Thatcher, J. and Wagner, E. [1978]. "An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types", in Current Trends in Programming Methodology, Yeh, R. (ed.), Vol. 4, Prentice-Ball, pp. 80-149.

Google Scholar

[2]

Bernot, G. [1986]. "Une Sémantique Algébrique pour une Spécification Différentiée des Exceptions et des Erreurs: Application á l' Implémentation et aux Primitives de Structuration des Spécifications Formelles", Thèse de Docteur de 3e Cycle, Centre d' Orsay, Université de Paris-Sud.

Google Scholar

[3]

Ehrig, H., Kreowski, H.-J., Mahr, B. and Padawitz, P. [1982]. "Algebraic Implementation of Abstract Data Types", Theoretical Computer Science, Vol. 20, pp. 209-263.

Crossref

Google Scholar

[4]

Guttag, J. V. [1977]. "Abstract Data Types and the Development of Data Structures", Communications of the ACM, Vol. 20, Num. 6, pp. 396-404.

Digital Library

Google Scholar

[5]

Guttag, J. V., Horowitz, E. and Musser, D. R. [1978]. "Abstract Data Types and Software Validation". Communications of the ACM. Vol. 21, Num. 12, pp. 1048-1064.

Digital Library

Google Scholar

[6]

Huet, G. and Oppen, C. [1980]. "Equations and Rewrite Rules: A Survey", in Formal Language Theory: Perspectives and Open Problems, Book, R. V. (ed.), Academic Press, New York, pp. 350-405.

Google Scholar

[7]

Goguen, J. A. and Meseguer, J. [1981]. "Completeness of Many-sorted Equational Logic", Sigplan Notices, Vol. 16, Num. 7, pp. 24-32.

Digital Library

Google Scholar

[8]

Goguen, J. A. and Meseguer, J. [1987]. "Remarks on Remarks on Many-Sorted Equational Logic", Sigplan Notices, Vol. 22, Num. 4, pp. 41-48.

Digital Library

Google Scholar

[9]

Meseguer, J. and Goguen, J. A. [1985a]. "Initiality, Induction and Computability", in Algebraic Methods in Semantics, Reynolds, J. C. (ed.), Cambridge University Press, pp. 459-541.

Digital Library

Google Scholar

[10]

Meseguer, J. and Goguen, J. A. [1985b]. "Deduction with Many-Sorted Rewrite Rules", Technical Report CSLI-85-42, Center for the Study of Language and Information, Stanford University.

Google Scholar

Index Terms

Remarks on many-sorted equational logic with respect to algebraic implementations
1. Computing methodologies
  1. Symbolic and algebraic manipulation
2. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Abstract data types

Recommendations

Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic

We show that the generalized variant of formal systems where the underlying equational specifications are membership equational theories, and where the rules are conditional and can have equations, memberships and rewrites in the conditions is ...
Completeness of many-sorted equational logic

The rules of deduction which are usually used for many-sorted equational logic in computer science, for example in the study of abstract data types, are not sound. Correcting these rules by introducing explicit quantifiers yields a system which, ...
Decidable fragments of many-sorted logic

Many natural specifications use types. We investigate the decidability of fragments of many-sorted first-order logic. We identified some decidable fragments and illustrated their usefulness by formalizing specifications considered in the literature. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGPLAN Notices Volume 23, Issue 1

Jan., 1988

128 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/44304

Editor:
Richard L. Wexelblat

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 January 1988

Published in SIGPLAN Volume 23, Issue 1

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

0
Total Citations
99
Total Downloads

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

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

References

Index Terms

Recommendations

Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic

Completeness of many-sorted equational logic

Decidable fragments of many-sorted logic

Comments

Information

Published In

Publisher

Publication History

Check for updates

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations