{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T14:55:19Z","timestamp":1761922519568,"version":"build-2065373602"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1999,9,1]],"date-time":"1999-09-01T00:00:00Z","timestamp":936144000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,9,1]],"date-time":"1999-09-01T00:00:00Z","timestamp":936144000000},"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":[[1999,9]]},"DOI":"10.1023\/a:1010052222987","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T00:56:42Z","timestamp":1040605002000},"page":"171-201","source":"Crossref","is-referenced-by-count":17,"title":["Computing with Contexts"],"prefix":"10.1007","volume":"12","author":[{"given":"Ian A.","family":"Mason","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"234970_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Cardeli, L., Curien, P.-L., and L\u00e9vy, J.-J. Explicit substitutions. In Seventeenth Annual ACM Symposium on Principles of Programmings Languages, 1990, pp. 31\u201346.","DOI":"10.1145\/96709.96712"},{"key":"234970_CR2","unstructured":"Aczel, P. A general Church-Rosser theorem, Unpublished manuscript."},{"key":"234970_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S095679689700261X","volume":"7","author":"G. Agha","year":"1997","unstructured":"Agha, G., Mason, I.A. Smith, S.F., and Talcott, C.L. A foundation for actor computation. Journal of Functional Programming, 7:1\u201372, 1997.","journal-title":"Journal of Functional Programming"},{"key":"234970_CR4","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BF00245294","volume":"9","author":"A. Avron","year":"1992","unstructured":"Avron, A., Honsell, F., Mason, I.A., and Pollack, R. Using typed lambda calculus to implement formal systems on a machine. Journal of Automated Reasoning, 9:309\u2013354, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"234970_CR5","unstructured":"Curry, H.B. and Feys, R. Combinatory Logic. Studies in Logic and the Foundations of Mathematics. North-Holland, 1958."},{"key":"234970_CR6","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/S0304-3975(97)00150-3","volume":"192","author":"L. Dami","year":"1998","unstructured":"Dami, L. A lambda-calculus for dynamic binding. Theoretical Computer Science, 192:201\u2013231, 1998.","journal-title":"Theoretical Computer Science"},{"key":"234970_CR7","unstructured":"Felleisen, M. The Calculi of Lambda-v-cs Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. Ph.D. Thesis, Indiana University, 1987."},{"key":"234970_CR8","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":"234970_CR9","unstructured":"Frost, J. and Mason, I.A. An operational logic of effects. In Proceedings of theAustralasian Theory Symposium, CATS' 96, 1996, pp. 147\u2013156."},{"key":"234970_CR10","doi-asserted-by":"crossref","unstructured":"Griffin, T.G. A formulae as types notion of control. In Seventeenth Annual ACM Symposium on Principles of Programmings Languages, 1990, pp. 47\u201358.","DOI":"10.1145\/96709.96714"},{"key":"234970_CR11","unstructured":"Hashimoto, M. and Ohori, A. A typed context calculus, 1996. Preprint RIMS-1098, Research Institute for Mathematical Sciences, Kyoto University, 1996. See: http:\/\/www.kurims.kyoto-u.ac.jp\/~ohori\/."},{"issue":"1","key":"234970_CR12","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):55\u201390, 1995.","journal-title":"Information and Computation"},{"key":"234970_CR13","unstructured":"Klop, J. Combinatory Reduction Systems. Ph.D. Thesis, University of Utrecht, 1980. Published as a Mathematical Centre Tract 129."},{"issue":"6","key":"234970_CR14","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1145\/232629.232652","volume":"31","author":"S.-D. Lee","year":"1996","unstructured":"Lee, S.-D. and Friedman, D.P. Enriching the Lambda Calculus with Contexts: Towards a Theory of Incremental Program Construction. In Proceedings ACM Int. Conf. on Functional Programming, ACM SIGPLAN Notices, 31(6):239\u2013250, 1996.","journal-title":"Proceedings ACM Int. Conf. on Functional Programming, ACM SIGPLAN Notices"},{"key":"234970_CR15","unstructured":"Mason, I.A. Hoare's Logic in the LF. Technical Report ECS-LFCS-87-32, Laboratory for foundations of computer science, University of Edinburgh, 1987."},{"key":"234970_CR16","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1016\/S0304-3975(97)00047-9","volume":"185","author":"I.A. Mason","year":"1997","unstructured":"Mason, I.A. A first order logic of effects. Theoretical Computer Science, 185:277\u2013318, 1997.","journal-title":"Theoretical Computer Science"},{"key":"234970_CR17","unstructured":"Mason, I.A. Parametric Computation. In Proceedings of the Australasian Theory Symposium, CATS' 97, J. Harland (Ed.), 1997, pp. 103\u2013112. Complete proofs of all claims are also available from http:\/\/smcs.une.edu.au\/ iam\/Data\/Papers\/97 cats-proofs.ps as postscript."},{"key":"234970_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:287\u2013327, 1991.","journal-title":"Journal of Functional Programming"},{"key":"234970_CR19","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:1\u201322, 1977.","journal-title":"Theoretical Computer Science"},{"key":"234970_CR20","unstructured":"Morris, J.H. Lambda Calculus Models of Programming Languages. Ph.D. Thesis, Massachusetts Institute of Technology, 1968."},{"key":"234970_CR21","unstructured":"Pitts, A.M. Some notes on inductive and co-inductive techniques in the semantics of functional programs, 1994. Notes Series BRICS-NS-94-5, BRICS, Department of Computer Science, University of Aarhus."},{"key":"234970_CR22","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:125\u2013159, 1975.","journal-title":"Theoretical Computer Science"},{"key":"234970_CR23","doi-asserted-by":"crossref","unstructured":"Sands, D. Computing with contexts--A simple approach. In Proceedings of Higher-Order Operational Techniques in Semantics, HOOTS II, Electronic Notes in Theoretical Computer Science, vol. 10, 1998.","DOI":"10.1016\/S1571-0661(05)80694-2"},{"key":"234970_CR24","unstructured":"Sato, M., Sakurai, T., and Burstall, R. Explicit environments. In Typed Lambda Calculi and Applications, Proceedings of 4th International Conference, TLCA'99. L'Aquila, Italy, April 7\u20139, 1999, J.Y. Girard (Ed.) vol. 1581 of Lecture Notes in Computer Science, Springer-Verlag, 1999."},{"key":"234970_CR25","doi-asserted-by":"crossref","unstructured":"Talcott, C.L. Binding structures. In Artificial Intelligence and Mathematical Theory of Computation. Vladimir Lifschitz (Ed.), Academic Press, 1991.","DOI":"10.1016\/B978-0-12-450010-5.50030-X"},{"key":"234970_CR26","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/0304-3975(93)90240-T","volume":"112","author":"C.L. Talcott","year":"1993","unstructured":"Talcott, C.L. A theory of binding structures and its applications to rewriting. Theoretical Computer Science, 112:99\u2013143, 1993.","journal-title":"Theoretical Computer Science"},{"key":"234970_CR27","unstructured":"Talcott, C.L. Reasoning about functions with effects. In Higher Order Operational Techniques in Semantics. A. Gordon and A. Pitts (Eds.), Cambridge University Press, 1998."},{"key":"234970_CR28","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0004-3702(80)90015-6","volume":"13","author":"R.W. Weyhrauch","year":"1980","unstructured":"Weyhrauch, R.W. Prolegomena to a theory of formal reasoning. Artificial Intelligence, 13:133\u2013170, 1980.","journal-title":"Artificial Intelligence"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1010052222987.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1010052222987\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1010052222987.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T13:50:38Z","timestamp":1751982638000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1010052222987"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,9]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1999,9]]}},"alternative-id":["234970"],"URL":"https:\/\/doi.org\/10.1023\/a:1010052222987","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"type":"print","value":"1388-3690"},{"type":"electronic","value":"1573-0557"}],"subject":[],"published":{"date-parts":[[1999,9]]}}}