{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:37:50Z","timestamp":1725457070809},"publisher-location":"Berlin\/Heidelberg","reference-count":27,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540579354"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0032403","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:30:32Z","timestamp":1134282632000},"page":"225-254","source":"Crossref","is-referenced-by-count":1,"title":["Program transformation via contextual assertions"],"prefix":"10.1007","author":[{"given":"Ian A.","family":"Mason","sequence":"first","affiliation":[]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"4","author":"K.R. Apt","year":"1981","unstructured":"K.R. Apt. Ten years of Hoare's logic: A survey-part I. ACM Transactions on Programming Languages and Systems, 4:431\u2013483, 1981.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"S. Feferman. A language and axioms for explicit mathematics. In Algebra and Logic, volume 450 of Springer Lecture Notes in Mathematics, pages 87\u2013139. Springer Verlag, 1975.","DOI":"10.1007\/BFb0062852"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"S. Feferman. Constructive theories of functions and classes. In Logic Colloquium '78, pages 159\u2013224. North-Holland, 1979.","DOI":"10.1016\/S0049-237X(08)71625-2"},{"key":"13_CR4","first-page":"95","volume":"19","author":"S. Feferman","year":"1985","unstructured":"S. Feferman. A theory of variable types. Revista Colombiana de Mat\u00e9maticas, 19:95\u2013105, 1985.","journal-title":"Revista Colombiana de Mat\u00e9maticas"},{"key":"13_CR5","series-title":"Volume 106 of Contemporary Mathematics","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1090\/conm\/106\/1057818","volume-title":"Logic and Computation","author":"S. Feferman","year":"1990","unstructured":"S. Feferman. Polymorphic typed lambda-calculi in a type-free axiomatic framework. In Logic and Computation, Volume 106 of Contemporary Mathematics, pages 101\u2013136. A.M.S., Providence R. I., 1990."},{"key":"13_CR6","unstructured":"M. Felleisen, 1993. Personal communication."},{"key":"13_CR7","unstructured":"M. Felleisen and D.P. Friedman. Control operators, the SECD-machine, and the \u03bb-calculus. In M. Wirsing, editor, Formal Description of Programming Concepts III, pages 193\u2013217. North-Holland, 1986."},{"key":"13_CR8","series-title":"Computer Systems Series","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5298.001.0001","volume-title":"Performance and Evaluation of Lisp Systems","author":"R. P. Gabriel","year":"1985","unstructured":"Richard P. Gabriel. Performance and Evaluation of Lisp Systems. Computer Systems Series. MIT Press, Cambridge, Massachusetts, 1985."},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"D. Harel. Dynamic logic. In D. Gabbay and G. Guenthner, editors, Handbook of Philosophical Logic, Vol. II, pages 497\u2013604. D. Reidel, 1984.","DOI":"10.1007\/978-94-009-6259-0_10"},{"key":"13_CR10","unstructured":"F. Honsell, I. A. Mason, S. F. Smith, and C. L. Talcott. A Variable Typed Logic of Effects. Information and Computation, ???(???):???\u2013???, 199?"},{"key":"13_CR11","series-title":"Volume ??? of Lecture Notes in Computer Science","first-page":"---","volume-title":"Proceedings of CSL92","author":"F. Honsell","year":"1993","unstructured":"F. Honsell, I. A. Mason, S. F. Smith, and C. L. Talcott. A theory of classes for a functional language with effects. In Proceedings of CSL92, Volume ??? of Lecture Notes in Computer Science, pages---\u2013---Springer, Berlin, 1993."},{"key":"13_CR12","unstructured":"U. J\u00f8 rring and W. L. Scherlis. Deriving and using destructive data types. In IFIP TC2 Working Conference on Program Specification and Transformation. North-Holland, 1986."},{"key":"13_CR13","unstructured":"I. A. Mason. The Semantics of Destructive Lisp. PhD thesis, Stanford University, 1986. Also available as CSLI Lecture Notes No. 5, Center for the Study of Language and Information, Stanford University."},{"key":"13_CR14","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/0167-6423(88)90026-3","volume":"10","author":"I. A. Mason","year":"1988","unstructured":"I. A. Mason. Verification of programs that destructively manipulate data. Science of Computer Programming, 10:177\u2013210, 1988.","journal-title":"Science of Computer Programming"},{"key":"13_CR15","unstructured":"I. A. Mason, J. D. Pehoushek, C. L. Talcott, and J. S. Weening. A Qlisp Primer. Technical Report STAN-CS-90-1340, Department of Computer Science, Stanford University, 1990."},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"I. A. Mason and C. L. Talcott. Axiomatizing operational equivalence in the presence of side effects. In Fourth Annual Symposium on Logic in Computer Science. IEEE, 1989.","DOI":"10.1109\/LICS.1989.39183"},{"key":"13_CR17","series-title":"Volume 372 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"574","DOI":"10.1007\/BFb0035784","volume-title":"Proceedings of the 16th EATCS Colloquium on Automata, Languages, and Programming","author":"I. A. Mason","year":"1989","unstructured":"I. A. Mason and C. L. Talcott. Programming, transforming, and proving with function abstractions and memories. In Proceedings of the 16th EATCS Colloquium on Automata, Languages, and Programming, Stresa, Volume 372 of Lecture Notes in Computer Science, pages 574\u2013588. Springer-Verlag, 1989."},{"key":"13_CR18","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1017\/S0956796800000125","volume":"1","author":"I. A. Mason","year":"1991","unstructured":"I. A. Mason and C. L. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1:287\u2013327, 1991.","journal-title":"Journal of Functional Programming"},{"issue":"2","key":"13_CR19","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/0304-3975(92)90301-U","volume":"105","author":"I. A. Mason","year":"1992","unstructured":"I. A. Mason and C. L. Talcott. Inferring the equivalence of functional programs that mutate data. Theoretical Computer Science, 105(2):167\u2013215, 1992.","journal-title":"Theoretical Computer Science"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"I. A. Mason and C. L. Talcott. References, local variables and operational reasoning. In Seventh Annual Symposium on Logic in Computer Science, pages 186\u2013197. IEEE, 1992.","DOI":"10.1109\/LICS.1992.185532"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"J. McCarthy. A basis for a mathematical theory of computation. In P. Braffort and D Herschberg, editors, Computer programming and formal systems, pages 33\u201370. North-Holland, 1963.","DOI":"10.1016\/S0049-237X(08)72018-4"},{"key":"13_CR22","unstructured":"E. Moggi. Computational lambda-calculus and monads. Technical Report ECS-LFCS-88-86, University of Edinburgh, 1988."},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"E. Moggi. Computational lambda-calculus and monads. In Fourth Annual Symposium on Logic in Computer Science. IEEE, 1989.","DOI":"10.1109\/LICS.1989.39155"},{"key":"13_CR24","unstructured":"J. H. Morris. Lambda calculus models of programming languages. PhD thesis, Massachusetts Institute of Technology, 1968."},{"key":"13_CR25","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/359461.359466","volume":"20","author":"J. H. Morris","year":"1976","unstructured":"J. H. Morris and B. Wegbreit. Subgoal induction. Communications of the Association for Computing Machinery, 20:209\u2013222, 1976.","journal-title":"Communications of the Association for Computing Machinery"},{"key":"13_CR26","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G. Plotkin","year":"1975","unstructured":"G. Plotkin. Call-by-name, call-by-value and the lambda calculus. Theoretical Computer Science, 1:125\u2013159, 1975.","journal-title":"Theoretical Computer Science"},{"key":"13_CR27","unstructured":"J.C. Reynolds. Idealized ALGOL and its specification logic. In D. N\u00e9el, editor, Tools and Notions for Program Construction, pages 121\u2013161. Cambridge University Press, 1982."}],"container-title":["Lecture Notes in Computer Science","Logic, Language and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0032403","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T13:47:40Z","timestamp":1586612860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0032403"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540579354"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/bfb0032403","relation":{},"subject":[]}}