{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T13:11:56Z","timestamp":1742994716387,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642253782"},{"type":"electronic","value":"9783642253799"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-25379-9_4","type":"book-chapter","created":{"date-parts":[[2011,11,14]],"date-time":"2011-11-14T01:33:47Z","timestamp":1321234427000},"page":"21-36","source":"Crossref","is-referenced-by-count":18,"title":["Proof-Carrying Code in a Session-Typed Process Calculus"],"prefix":"10.1007","author":[{"given":"Frank","family":"Pfenning","sequence":"first","affiliation":[]},{"given":"Luis","family":"Caires","sequence":"additional","affiliation":[]},{"given":"Bernardo","family":"Toninho","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","first-page":"27","volume-title":"Proceedings of the 5th Workshop on Types in Language Design and Implementation, TLDI 2010","author":"K. Avijit","year":"2010","unstructured":"Avijit, K., Datta, A., Harper, R.: Distributed programming with distributed authorization. In: Proceedings of the 5th Workshop on Types in Language Design and Implementation, TLDI 2010, pp. 27\u201338. ACM, New York (2010)"},{"issue":"4","key":"4_CR2","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1093\/logcom\/14.4.447","volume":"14","author":"S. Awodey","year":"2004","unstructured":"Awodey, S., Bauer, A.: Propositions as [types]. Journal of Logic and Computation\u00a014(4), 447\u2013471 (2004)","journal-title":"Journal of Logic and Computation"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. In: 21st Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, pp. 17\u201332. IEEE Computer Society (June 2008)","DOI":"10.1109\/CSF.2008.27"},{"issue":"2","key":"4_CR4","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1017\/S095679680400543X","volume":"15","author":"E. Bonelli","year":"2005","unstructured":"Bonelli, E., Compagnoni, A., Gunter, E.L.: Correspondence Assertions for Process Synchronization in Concurrent Communications. J. of Func. Prog.\u00a015(2), 219\u2013247 (2005)","journal-title":"J. of Func. Prog."},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-642-15375-4_16","volume-title":"CONCUR 2010 - Concurrency Theory","author":"L. Caires","year":"2010","unstructured":"Caires, L., Pfenning, F.: Session Types as Intuitionistic Linear Propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 222\u2013236. Springer, Heidelberg (2010)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-14458-5_1","volume-title":"Web Services and Formal Methods","author":"M. Dezani-Ciancaglini","year":"2010","unstructured":"Dezani-Ciancaglini, M., de\u2019Liguoro, U.: Sessions and Session Types: An Overview. In: Laneve, C., Su, J. (eds.) WS-FM 2009. LNCS, vol.\u00a06194, pp. 1\u201328. Springer, Heidelberg (2010)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/11863908_19","volume-title":"Computer Security \u2013 ESORICS 2006","author":"D. Garg","year":"2006","unstructured":"Garg, D., Bauer, L., Bowers, K.D., Pfenning, F., Reiter, M.K.: A Linear Logic of Authorization and Knowledge. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol.\u00a04189, pp. 297\u2013312. Springer, Heidelberg (2006)"},{"key":"#cr-split#-4_CR8.1","doi-asserted-by":"crossref","unstructured":"2. Garg, D., Pfenning, F.: A proof-carrying file system. In: Evans, D., Vigna, G. (eds.) Proceedings of the 31st Symposium on Security and Privacy (Oakland 2010), Berkeley, California. IEEE (May 2010)","DOI":"10.1109\/SP.2010.28"},{"key":"#cr-split#-4_CR8.2","unstructured":"3. Extended version available as Technical Report CMU-CS-09-123 (June 2009)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1007\/3-540-57208-2_35","volume-title":"CONCUR\u201993","author":"K. Honda","year":"1993","unstructured":"Honda, K.: Types for Dyadic Interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol.\u00a0715, pp. 509\u2013523. Springer, Heidelberg (1993)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/BFb0053567","volume-title":"Programming Languages and Systems","author":"K. Honda","year":"1998","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language Primitives and Type Discipline for Structured Communication-Based Programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol.\u00a01381, pp. 122\u2013138. Springer, Heidelberg (1998)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Mazurak, K., Zdancewic, S.: Lolliproc: To concurrency from classical linear logic via Curry-Howard and control. In: Hudak, P., Weirich, S. (eds.) Proceedings of the 15th International Conference on Functional Programming (ICFP 2010), Baltimore, Maryland, pp. 39\u201350. ACM (September 2010)","DOI":"10.1145\/1863543.1863551"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: Jones, N.D. (ed.) Conference Record of the 24th Symposium on Principles of Programming Languages (POPL 1997), Paris, France, pp. 106\u2013119. ACM Press (January 1997)","DOI":"10.1145\/263699.263712"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Lee, P.: Safe kernel extensions without run-time checking. In: Proceedings of the Second Symposium on Operating System Design and Implementation (OSDI 1996), Seattle, Washington, pp. 229\u2013243 (October 1996)","DOI":"10.1145\/238721.238781"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: Intensionality, extensionality, and proof irrelevance in modal type theory. In: Halpern, J. (ed.) Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS 2001), Boston, Massachusetts, pp. 221\u2013230. IEEE (June 2001)","DOI":"10.1109\/LICS.2001.932499"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Salvesen, A., Smith, J.M.: The strength of the subset type in Martin-L\u00f6f\u2019s type theory. In: 3rd Annual Symposium on Logic in Computer Science (LICS 1988), Edinburgh, Scotland, pp. 384\u2013391. IEEE (July 1988)","DOI":"10.1109\/LICS.1988.5135"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Swamy, N., Checn, J., Fournet, C., Strub, P.-Y., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: Danvy, O. (ed.) International Conference on Functional Programming (ICFP 2011), Tokyo, Japan. ACM (September 2011) (to appear)","DOI":"10.1145\/2034773.2034811"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/978-3-642-11957-6_28","volume-title":"Programming Languages and Systems","author":"N. Swamy","year":"2010","unstructured":"Swamy, N., Chen, J., Chugh, R.: Enforcing Stateful Authorization and Information Flow Policies in Fine. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 529\u2013549. Springer, Heidelberg (2010)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: Proceedings of the 13th International Symposium on Principles and Practice of Declarative Programming (PPDP 2011), pp. 161\u2013172. ACM ( July 2011)","DOI":"10.1145\/2003476.2003499"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-25379-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,14]],"date-time":"2025-03-14T01:22:18Z","timestamp":1741915338000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25379-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642253782","9783642253799"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25379-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}