{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T18:22:59Z","timestamp":1761848579135,"version":"build-2065373602"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order and Symbolic Computation"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1023\/a:1025689206562","type":"journal-article","created":{"date-parts":[[2003,9,23]],"date-time":"2003-09-23T22:47:08Z","timestamp":1064357228000},"page":"161-202","source":"Crossref","is-referenced-by-count":7,"title":["Formal Foundations of Operational Semantics"],"prefix":"10.1007","volume":"16","author":[{"given":"Jonathan","family":"Ford","sequence":"first","affiliation":[]},{"given":"Ian A.","family":"Mason","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5142636_CR1","unstructured":"Butler, R.W., Dutertre, B., Jamsek, D., Owre, S., and Griffioen, D. PVS finite set library, 1997. Available at http:\/\/pvs.csl.sri.com\/pvs\/libraries\/finite sets.dmp."},{"key":"5142636_CR2","series-title":"Technical report","volume-title":"WIFT\u2019 95:Workshop on Industrial-StrengthFormal Specification Techniques","author":"J. Crow","year":"1995","unstructured":"Crow, J., Owre, S., Rushby, J., Shankar, N., and Srivas, M. A tutorial introduction to PVS. Technical report, SRI International, 1995. Presented at WIFT\u2019 95:Workshop on Industrial-StrengthFormal Specification Techniques, Boca Raton, Florida."},{"key":"5142636_CR3","unstructured":"Felleisen, M. and Friedman, D.P. Control operators, the SECD-machine, and the \u03bb-calculus. In Formal Description of Programming Concepts III, M. Wirsing (Ed.). North-Holland, 1986, pp. 193\u2013217."},{"key":"5142636_CR4","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0304-3975(92)90014-7","volume":"103","author":"M. Felleisen","year":"1992","unstructured":"Felleisen, M. and Hieb, R. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 103 (1992) 235\u2013271.","journal-title":"Theoretical Computer Science"},{"key":"5142636_CR5","unstructured":"Ford, J. The Church-Rosser theorem in PVS, 2000. PVS dump file (2.4 Megabytes) available at http:\/\/mcs.une.edu.au\/~pvs\/."},{"key":"5142636_CR6","unstructured":"Ford, J. The CIU theorem in PVS, 2000. PVS dump file (approximately 17 Megabytes) available at http:\/\/mcs.une.edu.au\/~pvs\/."},{"key":"5142636_CR7","unstructured":"Ford, J. and Mason, I.A. Establishing a general context lemma in PVS. In Proceedings of the 2nd Australasian Workshop on Computational Logic, AWCL'01, G. Antoniou and G. Governatori (Eds.). 2001, pp. 75\u201391. Available as postscript from http:\/\/mcs.une.edu.au\/~iam\/Data\/Papers\/01awcl.ps."},{"key":"5142636_CR8","doi-asserted-by":"crossref","unstructured":"Ford, J. and Mason, I.A. Operational techniques in PVS\u2014A preliminary evaluation. In Proceedings of the Australasian Theory Symposium, CATS'01, C.J. Fidge (Ed.). Vol. 42 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 2001, pp. 124\u2013142. Available as postscript from http:\/\/mcs.une.edu.au\/~iam\/Data\/Papers\/01cats.ps.","DOI":"10.1016\/S1571-0661(04)80882-X"},{"key":"5142636_CR9","unstructured":"Ford, J., Mason, I.A., and Shankar, N. Lessons learned from formal developments in PVS, 2002. Presented at LICS'02 (within FLoC'02), Copenhagen."},{"key":"5142636_CR10","unstructured":"Ford, J. and Shankar, N. Verifying shostak. In The Proceedings of CADE-18 (within FLoC'02), Copenhagen, 2002."},{"issue":"1","key":"5142636_CR11","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1006\/inco.1995.1077","volume":"119","author":"F. Honsell","year":"1995","unstructured":"Honsell, F., Mason, I.A., Smith, S.F., and Talcott, C.L. A variable typed logic of effects. Information and Computation, 119(1) (1995) 55\u201390.","journal-title":"Information and Computation"},{"key":"5142636_CR12","unstructured":"Knuth, D.E. The T\nEXbook. Addison-Wesley, 1984."},{"key":"5142636_CR13","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","volume":"6","author":"P.J. Landin","year":"1964","unstructured":"Landin, P.J. The mechanical evaluation of expressions. Computer Journal, 6 (1964) 308\u2013320.","journal-title":"Computer Journal"},{"key":"5142636_CR14","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1145\/365230.365257","volume":"9","author":"P.J. Landin","year":"1966","unstructured":"Landin, P.J. The next 700 programming languages. Comm. ACM, 9 (1966) 157\u2013166.","journal-title":"Comm. ACM"},{"key":"5142636_CR15","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1023\/A:1010052222987","volume":"12","author":"I.A. Mason","year":"1999","unstructured":"Mason, I.A. Computing with contexts. Higher-Order and Symbolic Computation, 12 (1999) 171\u2013201.","journal-title":"Higher-Order and Symbolic Computation"},{"issue":"1","key":"5142636_CR16","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1006\/inco.1996.0061","volume":"128","author":"I.A. Mason","year":"1996","unstructured":"Mason, I.A., Smith, S.F., and Talcott, C.L. From operational semantics to domain theory. Information and Computation, 128(1) (1996) 26\u201347.","journal-title":"Information and Computation"},{"key":"5142636_CR17","doi-asserted-by":"crossref","unstructured":"Mason, I.A. and Talcott, C.L. Programming, transforming, and proving with function abstractions and memories. In Proceedings of the 16th EATCS Colloquium on Automata, Languages, and Programming, Stresa, Vol. 372 of Lecture Notes in Computer Science, Springer-Verlag, 1989, pp. 574\u2013588.","DOI":"10.1007\/BFb0035784"},{"key":"5142636_CR18","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1017\/S0956796800000125","volume":"1","author":"I.A. Mason","year":"1991","unstructured":"Mason, I.A. and Talcott, C.L. Equivalence in functional languages with effects. Journal of Functional Programming, 1 (1991) 287\u2013327.","journal-title":"Journal of Functional Programming"},{"key":"5142636_CR19","unstructured":"Mason, I.A. and Talcott, C.L. Feferman-Landin logic. In Reflections\u2014A Symposium Honoring Solomon Feferman on his 70th Birthday, W. Sieg, R. Sommer, and C. Talcott (Eds.). Lecture Notes in Logic, 2001."},{"key":"5142636_CR20","doi-asserted-by":"crossref","unstructured":"McKinna, J. and Pollack, R. Pure type systems formalized. In Typed Lambda Calculi and Applications, M. Bezem and J.F. Groote (Eds.). Vol. 664 of Lecture Notes in Computer Science, Springer Verlag, 1993, pp. 289\u2013305.","DOI":"10.1007\/BFb0037113"},{"key":"5142636_CR21","doi-asserted-by":"crossref","unstructured":"McKinna, J. and Pollack, R. Some lambda calculus and type theory formalized. Journal of Automated Reasoning, 23 (1999). An abridged version appeared as [20].","DOI":"10.1023\/A:1006294005493"},{"key":"5142636_CR22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(77)90053-6","volume":"4","author":"R. Milner","year":"1977","unstructured":"Milner, R. Fully abstract models of typed \u03bb-calculi. Theoretical Computer Science, 4 (1977) 1\u201322.","journal-title":"Theoretical Computer Science"},{"key":"5142636_CR23","unstructured":"Morris, J.H. Lambda Calculus Models of Programming Languages. Ph.D. thesis, Massachusetts Institute of Technology, 1968."},{"key":"5142636_CR24","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G. Plotkin","year":"1975","unstructured":"Plotkin, G. Call-by-name, call-by-value and the lambda calculus. Theoretical Computer Science, 1 (1975) 125\u2013159.","journal-title":"Theoretical Computer Science"},{"key":"5142636_CR25","unstructured":"Shankar, N. Personal communication, July 2000."},{"key":"5142636_CR26","unstructured":"Talcott, C.L. Reasoning about functions with effects. In Higher Order Operational Techniques in Semantics. Cambridge University Press, 1996."}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1025689206562.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1025689206562\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1025689206562.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T13:45:11Z","timestamp":1751982311000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1025689206562"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["5142636"],"URL":"https:\/\/doi.org\/10.1023\/a:1025689206562","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"type":"print","value":"1388-3690"},{"type":"electronic","value":"1573-0557"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}