{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T07:12:58Z","timestamp":1743059578303,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540926863"},{"type":"electronic","value":"9783540926870"}],"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-92687-0_6","type":"book-chapter","created":{"date-parts":[[2009,2,10]],"date-time":"2009-02-10T04:25:38Z","timestamp":1234239938000},"page":"76-91","source":"Crossref","is-referenced-by-count":2,"title":["The Logic of Proofs as a Foundation for Certifying Mobile Computation"],"prefix":"10.1007","author":[{"given":"Eduardo","family":"Bonelli","sequence":"first","affiliation":[]},{"given":"Federico","family":"Feller","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","first-page":"189","volume-title":"Handbook of Philosophical Logic","author":"S. Art\u00ebmov","year":"2004","unstructured":"Art\u00ebmov, S., Beklemishev, L.: Provability logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn., vol.\u00a013, pp. 189\u2013360. Kluwer, Dordrecht (2004)","edition":"2"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-540-72734-7_2","volume-title":"Logical Foundations of Computer Science","author":"S.N. Art\u00ebmov","year":"2007","unstructured":"Art\u00ebmov, S.N., Bonelli, E.: The intensional lambda calculus. In: Artemov, S.N., Nerode, A. (eds.) LFCS 2007. LNCS, vol.\u00a04514, pp. 12\u201325. Springer, Heidelberg (2007)"},{"key":"6_CR3","unstructured":"Artemov, S.: Operational modal logic. Technical Report MSI 95-29, Cornell Univsersity (1995)"},{"issue":"1","key":"6_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2687821","volume":"7","author":"S. Artemov","year":"2001","unstructured":"Artemov, S.: Explicit provability and constructive semantics. Bulletin of Symbolic Logic\u00a07(1), 1\u201336 (2001)","journal-title":"Bulletin of Symbolic Logic"},{"key":"6_CR5","volume-title":"Handbook of Modal Logics","author":"C. Areces","year":"2006","unstructured":"Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logics. Elsevier, Amsterdam (2006)"},{"key":"6_CR6","unstructured":"Bonelli, E., Feller, F.: The logic of proofs as a foundation for certifying mobile computation, \n                  \n                    http:\/\/www.lifia.info.unlp.edu.ar\/~eduardo\/lpCertFull.pdf"},{"issue":"4","key":"6_CR7","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1093\/comjnl\/43.4.274","volume":"43","author":"T. Borghuis","year":"2000","unstructured":"Borghuis, T., Feijs, L.M.G.: A constructive logic for services and information flow in computer networks. Comput. J.\u00a043(4), 274\u2013289 (2000)","journal-title":"Comput. J."},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: ICFP, pp. 233\u2013243 (2000)","DOI":"10.1145\/357766.351262"},{"key":"6_CR9","first-page":"511","volume":"11","author":"R. Davies","year":"2001","unstructured":"Davies, R., Pfenning, F.: A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science\u00a011, 511\u2013540 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"3","key":"6_CR10","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/382780.382785","volume":"48","author":"R. Davies","year":"2001","unstructured":"Davies, R., Pfenning, F.: A modal analysis of staged computation. J. ACM\u00a048(3), 555\u2013604 (2001)","journal-title":"J. ACM"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BFb0022247","volume-title":"Computer Science Logic","author":"H. Herbelin","year":"1995","unstructured":"Herbelin, H.: A lambda-calculus structure isomorphic to gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol.\u00a0933, pp. 61\u201375. Springer, Heidelberg (1995)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-540-24725-8_16","volume-title":"Programming Languages and Systems","author":"L. Jia","year":"2004","unstructured":"Jia, L., Walker, D.: Modal proofs as distributed programs (extended abstract). In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 219\u2013233. Springer, Heidelberg (2004)"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/11506676_5","volume-title":"Logic Based Program Synthesis and Transformation","author":"J. Moody","year":"2005","unstructured":"Moody, J.: Logical mobility and locality types. In: Etalle, S. (ed.) LOPSTR 2004. LNCS, vol.\u00a03573, pp. 69\u201384. Springer, Heidelberg (2005)"},{"key":"6_CR14","unstructured":"Murphy VII, T.: Modal Types for Mobile Code. PhD thesis, Carnegie Mellon (draft) (January 2008)"},{"key":"6_CR15","unstructured":"Simpson, A.: The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh (1994)"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Taha, W., Sheard, T.: Multi-stage programming. In: ICFP, p. 321 (1997)","DOI":"10.1145\/258949.258990"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Murphy VII, T., Crary, K., Harper, R.: Distributed control flow with classical modal logic. In: Ong, L. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 51\u201369. Springer, Heidelberg (2005)","DOI":"10.1007\/11538363_6"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Murphy VII, T., Crary, K., Harper, R.: Type-safe distributed programming with ml5. In: Barthe, G., Fournet, C. (eds.) TGC 2007 and FODO 2008. LNCS, vol.\u00a04912, pp. 108\u2013123. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78663-4_9"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Murphy VII, T., Crary, K., Harper, R., Pfenning, F.: A symmetric modal lambda calculus for distributed computing. In: LICS, pp. 286\u2013295. IEEE Computer Society, Los Alamitos (2004)","DOI":"10.1109\/LICS.2004.1319623"},{"issue":"3es","key":"6_CR20","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/289121.289129","volume":"30","author":"P. Wickline","year":"1998","unstructured":"Wickline, P., Lee, P., Pfenning, F., Davies, R.: Modal types as staging specifications for run-time code generation. ACM Comput. Surv.\u00a030(3es), 8 (1998)","journal-title":"ACM Comput. Surv."}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-92687-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T11:49:48Z","timestamp":1558266588000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-92687-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540926863","9783540926870"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-92687-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}