{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,12]],"date-time":"2023-01-12T16:59:39Z","timestamp":1673542779818},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,3,1]],"date-time":"2014-03-01T00:00:00Z","timestamp":1393632000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Log. Univers."],"published-print":{"date-parts":[[2014,3]]},"DOI":"10.1007\/s11787-014-0098-0","type":"journal-article","created":{"date-parts":[[2014,3,4]],"date-time":"2014-03-04T00:16:14Z","timestamp":1393892174000},"page":"103-140","source":"Crossref","is-referenced-by-count":3,"title":["Hypothetical Logic of Proofs"],"prefix":"10.1007","volume":"8","author":[{"given":"Eduardo","family":"Bonelli","sequence":"first","affiliation":[]},{"given":"Gabriela","family":"Steren","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,3,4]]},"reference":[{"key":"98_CR1","doi-asserted-by":"crossref","unstructured":"Artemov, S.N., Beklemishev, L.D.: Provability logic. In: Handbook of Philosophical Logic, 2nd ed, 13, pp. 189\u2013360. Springer, New York (2005)","DOI":"10.1007\/1-4020-3521-7_3"},{"key":"98_CR2","doi-asserted-by":"crossref","unstructured":"Sergei, N.: Art\u00ebmov and Eduardo Bonelli. The intensional lambda calculus. In: Art\u00ebmov, S.N., Nerode, A. (eds.) LFCS, vol. 4514 of Lecture Notes in Computer Science, pp. 12\u201325. Springer, New York (2007)","DOI":"10.1007\/978-3-540-72734-7_2"},{"key":"98_CR3","unstructured":"Abadi, M., Fournet, C.: Access control based on execution history. In: In Proceedings of the 10th Annual Network and Distributed System Security Symposium, pp. 107\u2013121, (2003)"},{"issue":"2","key":"98_CR4","doi-asserted-by":"crossref","first-page":"439","DOI":"10.2178\/jsl\/1185803617","volume":"72","author":"N. Sergei","year":"2007","unstructured":"Sergei N.: Art\u00ebmov and Rosalie Iemhoff. The basic intuitionistic logic of proofs. J. Symb. Log. 72(2), 439\u2013 (2007)","journal-title":"J. Symb. Log."},{"key":"98_CR5","unstructured":"Art\u00ebmov, S.: Operational modal logic. Technical Report Technical Report MSI 95-29, Cornell University (1995)"},{"issue":"1","key":"98_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2687821","volume":"7","author":"N. Sergei","year":"2001","unstructured":"Sergei N.: Art\u00ebmov. Explicit provability and constructive semantics. Bull. Symbolic Logic 7(1), 1\u2013 (2001)","journal-title":"Bull. Symbolic Logic"},{"key":"98_CR7","doi-asserted-by":"crossref","unstructured":"Bavera, F., Bonelli, E.: Justification logic and history based computation. In: Cavalcanti, A., D\u00e9harbe, D., Gaudel, M., Woodcock, J. (eds.) ICTAC, vol. 6255 of Lecture Notes in Computer Science, pp. 337\u2013351. Springer, New York (2010)","DOI":"10.1007\/978-3-642-14808-8_23"},{"issue":"7","key":"98_CR8","doi-asserted-by":"crossref","first-page":"935","DOI":"10.1016\/j.apal.2011.09.007","volume":"163","author":"E. Bonelli","year":"2012","unstructured":"Bonelli E., Feller F.: Justification logic as a foundation for certifying mobile computation. Ann. Pure Appl. Logic 163(7), 935\u2013950 (2012)","journal-title":"Ann. Pure Appl. Logic"},{"key":"98_CR9","doi-asserted-by":"crossref","unstructured":"Banerjee, A., Naumann, D.A.: History-based access control and secure information flow. In: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, International Workshop (CASSIS 2004), Revised Selected Papers, vol. 3362 of Lecture Notes in Computer Science, pp. 27\u201348. Springer-Verlag, Berlin (2005)","DOI":"10.1007\/978-3-540-30569-9_2"},{"issue":"4","key":"98_CR10","doi-asserted-by":"crossref","first-page":"665","DOI":"10.1093\/logcom\/exp041","volume":"21","author":"E. Dashkov","year":"2011","unstructured":"Dashkov E.: Arithmetical completeness of the intuitionistic logic of proofs. J. Log. Comput. 21(4), 665\u2013682 (2011)","journal-title":"J. Log. Comput."},{"key":"98_CR11","doi-asserted-by":"crossref","unstructured":"de Groote, P.: Strong normalization of classical natural deduction with disjunction. In: Typed Lambda Calculi and Applications, pp. 182\u2013196. Springer, New York (2001)","DOI":"10.1007\/3-540-45413-6_17"},{"key":"98_CR12","doi-asserted-by":"crossref","unstructured":"Davies, R., Pfenning, F.: A modal analysis of staged computation. In: Hans-Juergen B., Guy L.S. Jr. (eds.) POPL, pp. 258\u2013270. ACM Press, New York (1996)","DOI":"10.1145\/237721.237788"},{"key":"98_CR13","unstructured":"Kuznets, R.: A note on the use of sum in the logic of proofs (2009)"},{"key":"98_CR14","unstructured":"L\u00e9vy, J.-J.: R\u00e9ductions correctes et optimales dans le lambda-calcul. PhD thesis, Paris 7 (1978)"},{"key":"98_CR15","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Trans. Comput. Log. 9(3), 23:1\u201323:49 (2008)","DOI":"10.1145\/1352582.1352591"},{"key":"98_CR16","doi-asserted-by":"crossref","unstructured":"Parigot, M.: Lambda-mu-calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR, vol. 624 of Lecture Notes in Computer Science, pp. 190\u2013201. Springer, New York (1992)","DOI":"10.1007\/BFb0013061"},{"issue":"4","key":"98_CR17","doi-asserted-by":"crossref","first-page":"1461","DOI":"10.2307\/2275652","volume":"62","author":"M. Parigot","year":"1997","unstructured":"Parigot M.: Proofs of strong normalisation for second order classical natural deduction. J. Symbolic Logic 62(4), 1461\u20131479 (1997)","journal-title":"J. Symbolic Logic"},{"issue":"4","key":"98_CR18","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1017\/S0960129501003322","volume":"11","author":"F. Pfenning","year":"2001","unstructured":"Pfenning F., Davies R.: A judgmental reconstruction of modal logic. Math. Struct. Comput. Sci. 11(4), 511\u2013540 (2001)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"2","key":"98_CR19","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G.D. Plotkin","year":"1975","unstructured":"Plotkin G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125\u2013159 (1975)","journal-title":"Theor. Comput. Sci."},{"key":"98_CR20","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.entcs.2013.12.013","volume":"300","author":"G. Steren","year":"2014","unstructured":"Steren G., Bonelli E.: Intuitionistic hypothetical logic of proofs. Electr. Notes Theor. Comput. Sci. 300, 89\u2013103 (2014)","journal-title":"Electr. Notes Theor. Comput. Sci."}],"container-title":["Logica Universalis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-014-0098-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11787-014-0098-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-014-0098-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,8]],"date-time":"2019-08-08T03:48:12Z","timestamp":1565236092000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11787-014-0098-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3]]},"references-count":20,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,3]]}},"alternative-id":["98"],"URL":"https:\/\/doi.org\/10.1007\/s11787-014-0098-0","relation":{},"ISSN":["1661-8297","1661-8300"],"issn-type":[{"value":"1661-8297","type":"print"},{"value":"1661-8300","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,3]]}}}