{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T19:45:44Z","timestamp":1743018344906,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710653"},{"type":"electronic","value":"9783540710677"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-71067-7_22","type":"book-chapter","created":{"date-parts":[[2008,10,3]],"date-time":"2008-10-03T08:55:16Z","timestamp":1223024116000},"page":"262-277","source":"Crossref","is-referenced-by-count":1,"title":["Formalizing Soundness of Contextual Effects"],"prefix":"10.1007","author":[{"given":"Polyvios","family":"Pratikakis","sequence":"first","affiliation":[]},{"given":"Jeffrey S.","family":"Foster","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Hicks","sequence":"additional","affiliation":[]},{"given":"Iulian","family":"Neamtiu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Aydemir, B., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: POPL (2008)","key":"22_CR1","DOI":"10.1145\/1328438.1328443"},{"unstructured":"The Coq proof assistant., http:\/\/coq.inria.fr","key":"22_CR2"},{"unstructured":"Hicks, M., Foster, J.S., Pratikakis, P.: Lock Inference for Atomic Sections. In: TRANSACT (2006)","key":"22_CR3"},{"doi-asserted-by":"crossref","unstructured":"Igarashi, A., Kobayashi, N.: Resource Usage Analysis. In: POPL (2002)","key":"22_CR4","DOI":"10.1145\/503272.503303"},{"unstructured":"Lucassen, J.M.: Types and Effects: Towards the Integration of Functional and Imperative Programming. PhD thesis, MIT Laboratory for Computer Science, MIT\/LCS\/TR-408 (August 1987)","key":"22_CR5"},{"doi-asserted-by":"crossref","unstructured":"Neamtiu, I., Hicks, M., Foster, J.S., Pratikakis, P.: Contextual Effects for Version-Consistent Dynamic Software Updating and Safe Concurrent Programming. Technical Report CS-TR-4920, Dept. of Computer Science, University of Maryland (November 2007)","key":"22_CR6","DOI":"10.1145\/1328897.1328447"},{"doi-asserted-by":"crossref","unstructured":"Neamtiu, I., Hicks, M., Foster, J.S., Pratikakis, P.: Contextual effects for version-consistent dynamic software updating and safe concurrent programming. In: POPL (2008)","key":"22_CR7","DOI":"10.1145\/1328438.1328447"},{"key":"22_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)"},{"doi-asserted-by":"crossref","unstructured":"Skalka, C., Smith, S., Horn, D.V.: Types and trace effects of higher order programs. Journal of Functional Programming (July 2007)","key":"22_CR9","DOI":"10.1017\/S0956796807006466"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Languages and Systems","author":"F. Smith","year":"2000","unstructured":"Smith, F., Walker, D., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000 and ETAPS 2000. LNCS, vol.\u00a01782. Springer, Heidelberg (2000)"},{"issue":"2","key":"22_CR11","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1006\/inco.1994.1046","volume":"111","author":"J.-P. Talpin","year":"1994","unstructured":"Talpin, J.-P., Jouvelot, P.: The type and effect discipline. Inf. Comput.\u00a0111(2), 245\u2013296 (1994)","journal-title":"Inf. Comput."},{"doi-asserted-by":"crossref","unstructured":"Walker, D., Crary, K., Morrisett, G.: Typed memory management in a calculus of capabilities. In: TOPLAS, July 2000, vol.\u00a024(4), pp. 701\u2013771 (2000)","key":"22_CR12","DOI":"10.1145\/363911.363923"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71067-7_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T07:49:27Z","timestamp":1557820167000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71067-7_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540710653","9783540710677"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71067-7_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}