Hostname: page-component-cd9895bd7-q99xh Total loading time: 0 Render date: 2024-12-22T20:39:19.906Z Has data issue: false hasContentIssue false
  • English
  • Français

On the formalization of semantic conventions

Published online by Cambridge University Press:  12 March 2014

James G. Williams
James G. Williams*
Affiliation:
The Mitre Corporation, Bedford, Massachusetts 01730
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper discusses six formalization techniques, of varying strengths, for extending a formal system based on traditional mathematical logic. The purpose of these formalization techniques is to simulate the introduction of new syntactic constructs, along with associated semantics for them. We show that certain techniques (among the six) subsume others. To illustrate sharpness, we also consider a selection of constructs and show which techniques can and cannot be used to introduce them. The six studied techniques were selected on the basis of actual practice in logic and computing. They do not form an exhaustive list.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 55 , Issue 1 , March 1990 , pp. 220 - 243
Copyright
Copyright © Association for Symbolic Logic 1990

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[ABEL85]Abelson, H. and Sussman, G. J., Structure and interpretation of computer programs, MIT Press, Cambridge, Massachusetts, 1985.Google Scholar
[BAUE85]Bauer, F. L.et al., The Munich project CIP. I: The wide spectrum language CIP-L, Lecture Notes in Computer Science, vol. 183, Springer-Verlag, Berlin, 1985.CrossRefGoogle Scholar
[BLED86]Bledsoe, W. W., Some thoughts on proof discovery (Paper 86CH2340-8), Proceedings of the 1986 symposium on logic programming (Salt Lake City, Utah), IEEE Computer Society Press, Washington, D.C., 1986, pp. 2–10.Google Scholar
[BOYE79]Boyer, R. and Moore, J., A computational logic, Academic Press, New York, 1979.Google Scholar
[COQU86]Coquand, T. and Huet, G., The calculus of constructions, Information and Control, vol. 76 (1988), pp. 95–120.Google Scholar
[CRAI85]Craioen, D. and Good, D., Overview of the section “Verification systems”, Software Engineering Notes, vol. 10 (1985), no. 4, p. 1.CrossRefGoogle Scholar
[CULI77]Culik, K., Basic concepts of computer science and logic, Logic, foundations of mathematics and computability theory, Reidel, Dordrecht, 1977, pp. 237–266.CrossRefGoogle Scholar
[CURR58]Curry, H. B. and Feys, R., Combinatory logic. Vol. I, North-Holland, Amsterdam, 1958.Google Scholar
[ENDE72]Enderton, H. B., A mathematical introduction to logic, Academic Press, New York, 1972.Google Scholar
[GOGU77]Goguen, J. A., Initial algebra semantics and continuous algebras, Journal of the Association for Computing Machinery, vol. 24 (1977), pp. 68–95.CrossRefGoogle Scholar
[GORD70]Gordon, M. J. C, The denotational description of programming languages, an introduction, Springer-Verlag, Berlin, 1970.Google Scholar
[JECH78]Jech, T. J., Set theory, Academic Press, New York, 1978.Google Scholar
[KUNE83]Kunen, K., Set theory: an introduction to independence proofs, North-Holland, Amsterdam 1983.Google Scholar
[ŁUKA39]Łukasiewicz, J., The equivalential calculus, Polish logic 1920–1939 (McCall, S., editor), Oxford University Press, Oxford, 1967, pp. 88–115.Google Scholar
[MANN85]Manna, Z. and Waldinger, R., The logical basis for computer programming, Addison-Wesley, Reading, Massachusetts, 1985.Google Scholar
[NER059]Nerode, A., Composita, equations, and freely generated algebras, Transactions of the American Mathematical Society, vol. 91 (1959), pp. 139–151.CrossRefGoogle Scholar
[RICK75]Rickey, V. F., Creative definitions in propositional calculi, Notre Dame Journal of Formal Logic, vol. 16 (1975), pp. 273–294.CrossRefGoogle Scholar
[SAAL86]Saaltink, M., The mathematics of m-Verdi, Report FR-86-5420-03, I. P. Sharp Associates, Ottawa, 1986.Google Scholar
[STOY77]Stoy, J. E., Denotational semantics: the Scott-Strachey approach to programming language theory, MIT Press, Cambridge, Massachusetts, 1977.Google Scholar
[TURN79]Turner, D. A., A new implementation technique for applicative languages, Software—practice and experience, vol. 9 (1979), pp. 31–49.CrossRefGoogle Scholar
[WILL87]Williams, J. G., Formally grounded software reasoning systems: theory and requirements, Report MTP-266, The MITRE Corporation, Bedford, Massachusetts, 1987.Google Scholar