A mathematical approach to language design

ABSTRACT

A framework for validating surface properties of programming language constructs, composed of proof rules (akin to those of Hoare) and supporting hypotheses, is constructed using the mathematical semantics of Scott and Strachey. The following approach to language design is then considered: the constructs of a language should have surface properties which 1) need few hypotheses other than assumed surface properties; and 2) have proofs consisting, as far as possible, of trivial fixpoint and structural inductions.

REFERENCES

• 1: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 2: C. A. R. Hoare, Procedures and Parameters: An Axiomatic Approach, Symposium on Semantics of Algorithmic Languages, S.-Verlag, (1971),1O2-117.
• 3: C. A. R. Hoare, Hints on programming language design., Stanford University, Stanford, CA, 1973
• 4: P. Landin, The Mechanical Evaluation of Expressions, Computer Journal 6, (1964), 308-320.
• 5: G. T. Ligler, D.Phil.Thesis, Oxford University, (1975), in preparation.
• 6: Zohar Manna , Jean Vuillemin, Fixpoint approach to the theory of computation, Communications of the ACM, v.15 n.7, p.528-536, July 1972 [doi>10.1145/361454.361460]
• 7: R. E. Milne, The formal semantics of computer languages and their implementations, Ph.D,Thesis, Cambridge University, and Technical Monograph PRG-13, Oxford University Computing Laboratory, Programming Research Group, (1974).
• 8: Robin Milner, Implementation and applications of Scott's logic for computable functions, ACM SIGPLAN Notices, v.7 n.1, p.1-6, January 1972
• 9: James H. Morris, Jr., Types are not sets, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.120-124, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512938]
• 10: P. D. Mosses, The mathematical semantics of Algol 60, Technical Monograph PRG-12, O.U.C.L., Programming Research Group, (1974).
• 11: P. D. Mosses, Mathematical Semantics and Compiler-Generation, D.Phil. Thesis, Oxford University, (1974).
• 12: John C. Reynolds, On the Relation between Direct and Continuation Semantics, Proceedings of the 2nd Colloquium on Automata, Languages and Programming, p.141-156, July 29-August 02, 1974
• 13: M. Richards, The BCPL Reference Manual, Technical Memorandum 69/1, Cambridge U. Mathematical Laboratory, (1969).
• 14: D. Scott, Outline of a Mathematical Theory of Computation, Proc. Fourth Annual Princeton Conference on Information Sciences and Systems, pp.169-176, and Technical Monograph PRG-2, O.U.C.L., Programming Research Group, (1970).
• 15: D. Scott, Continuous Lattices, Proc. 1971 Dalhousie Conference, Springer Lecture Note Series, and Technical Monograph PRG-7, O.U.C.L., Programming Research Group, (1970).
• 16: D. Scott, Mathematical Concepts in Programming Language Semantics, AFIPS Conference Proceedings, Vol.40, (1972), 225-234.
• 17: D. Scott and C. Strachey, Toward a Mathematical Semantics for Computer Languages, Proc.Symp. on Computers and Automata, Polytechnic Institute of Brooklyn, and Technical Monograph PRG-6,O.U.C.L.,Prog.Res. Group, (1971).
• 18: C. Strachey, Towards a Formal Semantics, Formal Language Description Languages for Computer Programming, (ed. T. Steel), North-Holland,(1966), 198-220.
• 19: C. Strachey, Fundamental Concepts in Programming Languages, Unpublished, (1970).
• 20: C. Strachey, Varieties of Programming Language, Proc. International Computing Symposium, pp.222-233,Cini Foundation, Venice, and Technical Monograph PRG-10, Oxford University Computing Laboratory, Programming Research Group, (1972).
• 21: C. Strachey and C. Wadsworth, Continuations---A Mathematical Semantics for Full Jumps and Labels, Technical Monograph PRG-11, Oxford University Computing Laboratory, Programming Research Group, (1974).
• 22: R. D. Tennent, A Contribution to the Development of Pascal-Like Languages, Technical Report No. 74-25, Department of Computing and Information Science, Queen's University, Ontario, (1974).
• 23: C. Wadsworth, The Semantics and Prag-Matics of the λ-Calculus, D.Phil. Thesis, Oxford University, (1971).