Mitchell Wand
- 1 BACKUS, J. Programming language semantics and closed applicative languages. In Proceedings of the First ACM Symposium on Principles of Programming Languages, Boston, 1973, pp. 71-86. Google Scholar
- 2 BJORNER, D., AND JONES, C.B. (Eds.) Lecture Notes in Computer Science, vol. 61: The Vienna Development Method: The MetaoLanguage. Springer-Verlag, New York, 1978. Google Scholar
- 3 BURSTALL, R.M., AND DARLINGTON, g. A transformation system for developing recursive programs. J. ACM 24, i (Jan. 1977), 44-67. Google Scholar
- 4 BURSTALL, R.M., AND LANmN, P.J. Programs and their proofs: An algebraic approach. In Machine Intelligence, vol. 4, B. Meltzer and D. Michie (Eds.). Elsevier North-Holland, New York, 1969, pp. 17-44.Google Scholar
- 5 GOGUEN, J.A., THATCHER, J.W., WAONER, E.G., AND WRIGHT, J.B. Initial algebra semantics and continuous algebras. J. ACM 24, I (Jan. 1977), 68-95. Google Scholar
- 6 HOARE, C.A.R. Proving correctness of data representations. Acta Inf. 1, 4 (1972), 271-281.Google Scholar
- 7 JONES, N.D., AND SCHMIDT, S. Compiler generation from denotational semantics. In Lecture Notes in Computer Science, vol. 94: Semantics-Directed Compiler Generation, N.D. Jones (Ed.) Springer-Verlag, New York, 1980, pp. 70-93. Google Scholar
- 8 KNUTH, D.E. The Art of Computer Programming, vol. 1: Fundamental Algorithms. 2d ed. Addison-Wesley, Reading, Mass., 1973. Google Scholar
- 9 LANDIN, P.J. The mechanical evaluation of expressions. Computer J. 6, 4 (Jan. 1964), 308-320.Google Scholar
- 10 MCCARTHY, J. Towards a mathematical science of computation. Information Processing 62, C.M. PoppleweU (Ed.) Elsevier North-Holland, New York, 1963, pp. 21-28.Google Scholar
- 11 MCCARTHY, J., ANO PAINTER, J. Correctness of a compiler for arithmetic expressions. In Mathematical Aspects of Computer Science, vol. 19: Proceedings of Symposium in Applied Mathematics, J.T. Schwartz (Ed.) American Mathematical Society, Providence, R.I., 1967, pp. 33-41.Google Scholar
- 12 MILNE, R., AND STRACHEY, C. A Theory of Programming Language Semantics. Wiley, New York, 1976. Google Scholar
- 13 MILNER, R., AND WEYHRAUCH, R. Proving compiler correctness in a mechanized logic. In Machine Intelligence, vol. 7, B. Meltzer and D. Michie (Eds.). Edinburgh University Press, Edinburgh, Scotland, 1972, pp. 51-72.Google Scholar
- 14 MORRIS, J.H., JR. ANO WEOBREIT, B. Subgoal induction. Commun. ACM 20, 4 (Apr. 1977), 209-222. Google Scholar
- 15 MORRIS, L. Advice on structuring compilers and proving them correct. In Proceedings of the ACM Symposium on Principles of Programming Languages, Boston, 1973, pp. 144-152. Google Scholar
- 16 MOSSES, P. A constructive approach to compiler correctness. In Lecture Notes in Computer Science, vol. 85: Automata, Languages, and Programming, 7th Colloquium, Noordwijkerhout, The Netherlands, July 14-18, 1980, J.W. de Bakker and J. van Leeuwen (Eds.). Springer-Verlag, New York, 1980, pp. 449-469. Google Scholar
- 17 PLOTKIN, G.D. LCF considered as a programming language. Theor. Comput. Sci. 5, 3 (Dec. 1977), 223-255.Google Scholar
- 18 PRATT, T.W. Programming Languages: Design andlmplementation. Prentice-Hall, Englewood Cliffs, N.J., 1975. Google Scholar
- 19 QUlNE, W.V.O. Word and Object. M.I.T. Press, Cambridge, Mass., 1960.Google Scholar
- 20 REYNOLDS, J.C. On the relation between direct and continuation semantics. In Lecture Notes in Computer Science, vol. 14: Proceedings of the 2nd Colloquium on Automata, Languages, and Programming (Saarbrucken, 1974). Springer-Verlag, New York, 1974, pp. 141-156. Google Scholar
- 21 REYNOLOS, J.C. Definitional interpreters for higher-order programming languages. In Proceedings of the ACM Annual Conference, Boston, Aug. 1972, vol. 2, pp. 717-740. Google Scholar
- 22 SETm, R. Circular expressions: A progress report on semantics-directed compiler generation. In Lecture Notes in Computer Science, vol. 115: Automata, Languages, and Programming, 8th Colloquium, Acre, Israel, July 13-17, 1981, S. Even and O. Kariv (Eds.). Springer-Verlag, New York, 1981.Google Scholar
- 23 SETHI, R., AND TANG, A. Constructing call-by-value continuation semantics. J. ACM 27, 3 (July 1980), 580-597. Google Scholar
- 24 STEELE, G.L., AND SUSSMAN, G.J. The dream of a lifetime: A lazy scoping mechanism. In Conference Record of the 1980 LISP Conference, Stanford, Calif., 1980, pp. 163-172. Google Scholar
- 25 STEELE, G.L., JR. AND SUSSMAN, G.J. Design of a LiSP-based microprocessor. Commun. ACM 23, 11 (Nov. 1980), 628-645. Google Scholar
- 26 STOY, J.E. The congruence of two programming language definitions. Theor. Comput. Sci. 13 (1981), 151-174.Google Scholar
- 27 STOY, J.E. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. M.I.T. Press, Cambridge, Mass., 1977. Google Scholar
- 28 SUSSMAN, G.J., ANY STEELE, G.L., JR. SCHEME: An interpreter for extended lambda calculus. AI Memo 349, Massachusetts Institute of Technology, Cambridge, Mass., Dec. 1975. Google Scholar
- 29 TANENBAUM, A.S. Structured Computer Organization. Prentice-Hall, Englewood Cliffs, N.J., 1976. Google Scholar
- 30 TENNENT, R.D. The denotational semantics of programming languages. Commun. ACM 19, 8 (Aug. 1976), 437-453. Google Scholar
- 31 TnATCI~ER, J.W., WAG~ER, E.G., AND WRIGUT, J.B. More on advice on structuring compilers and proving them correct. In Lecture Notes in Computer Science, vol. 71: Automata, Languages, and Programming, 6th Colloquium, Graz, July 1979, H.A. Maurer (Ed.). Springer-Verlag, New York, 1979, pp. 596-615. Google Scholar
- 32 TURNER, D.A. A new implementation technique for applicative languages. Softw. Pract. Exper. 9 (1979), 31-49.Google Scholar
- 33 WANO, M. Semantics-directed machine architecture. In Conference Record of the 9th Annual ACM Symposium on Principles of Programming Languages, Albuquerque, Jan. 25-27, 1982, pp. 234-241. Google Scholar
- 34 WANO, M. First-order identities as a defining language. Acta Inf. 14 (1980), 337-357.Google Scholar
- 35 WANI), M. SCHEME version 3.1 reference manual. Tech. Rep. 93, Computer Science Dep., Indiana Univ., June 1980.Google Scholar
- 36 WANO, M. Continuation-based program transformation strategies. J. ACM 27, 1 (Jan. 1980), 164-180. Google Scholar
Index Terms
- Deriving Target Code as a Representation of Continuation Semantics
Recommendations
A Formal Semantics for P-Code
Verified Software. Theories, Tools and Experiments.AbstractDecompilation is currently a widely used tool in reverse engineering and exploit detection in binaries. Ghidra, developed by the National Security Agency, is one of the most popular decompilers. It decompiles binaries to high P-Code, from which ...
Deriving Pretty-Big-Step Semantics from Small-Step Semantics
Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410Big-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 ...
Deriving Operational Semantics from Denotational Semantics for Verilog
APSEC '01: Proceedings of the Eighth Asia-Pacific on Software Engineering ConferenceThis paper presents the derivation of an operational semantics from a denotational semantics for a subset of thewidely used hardware description language Verilog.Ouraim is to build equivalence between the operational and denotational semantics.We ...
Comments