{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T02:40:14Z","timestamp":1718332814674},"reference-count":47,"publisher":"Oxford University Press (OUP)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Logic Computation"],"DOI":"10.1093\/logcom\/exv090","type":"journal-article","created":{"date-parts":[[2016,1,31]],"date-time":"2016-01-31T01:28:22Z","timestamp":1454203702000},"page":"exv090","source":"Crossref","is-referenced-by-count":0,"title":["The first-order hypothetical logic of proofs"],"prefix":"10.1093","author":[{"given":"Gabriela","family":"Steren","sequence":"first","affiliation":[]},{"given":"Eduardo","family":"Bonelli","sequence":"additional","affiliation":[]}],"member":"286","published-online":{"date-parts":[[2016,1,30]]},"reference":[{"key":"2016013017281538000_exv090v1.1","doi-asserted-by":"publisher","DOI":"10.2307\/2687821"},{"key":"2016013017281538000_exv090v1.2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87803-2_1"},{"key":"2016013017281538000_exv090v1.3","unstructured":"Art\u00ebmov S. N. Operational modal logic. Technical Report MSI 95-29, Cornell University, 1995."},{"key":"2016013017281538000_exv090v1.4","doi-asserted-by":"publisher","DOI":"10.1017\/S1755020308090060"},{"key":"2016013017281538000_exv090v1.5","doi-asserted-by":"crossref","unstructured":"Art\u00ebmov S. N. Bonelli E. The intensional lambda calculus. In LFCS, pp. 12\u201325. Springer, 2007.","DOI":"10.1007\/978-3-540-72734-7_2"},{"key":"2016013017281538000_exv090v1.6","unstructured":"M. Abadi and C. Fournet. Access control based on execution history. In Proceedings of the 10th Annual Network and Distributed System Security Symposium, pp. 107\u2013121. The Internet Society, 2003."},{"key":"2016013017281538000_exv090v1.7","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1185803617"},{"key":"2016013017281538000_exv090v1.8","doi-asserted-by":"crossref","first-page":"475","DOI":"10.17323\/1609-4514-2001-1-4-475-490","article-title":"On first order logic of proofs","volume":"1","author":"Art\u00ebmov","year":"2001","journal-title":"Moscow Mathematical Journal"},{"key":"2016013017281538000_exv090v1.9","unstructured":"S. N. Art\u00ebmov and T. Yavorskaya (Sidon). First-order logic of proofs. Technical Report TR\u20132011005, CUNY Ph.D. Program in Computer Science, 2011."},{"key":"2016013017281538000_exv090v1.10","doi-asserted-by":"crossref","unstructured":"Bavera F. Bonelli E. Justification logic and history based computation. In ICTAC, pp. 337\u2013351. Springer, 2010.","DOI":"10.1007\/978-3-642-14808-8_23"},{"key":"2016013017281538000_exv090v1.11","doi-asserted-by":"crossref","unstructured":"Bavera F. Bonelli E. Justification logic and audited computation. Journal of Logic and Computation, 2015. doi: 10.1093\/logcom\/exv037.","DOI":"10.1093\/logcom\/exv037"},{"key":"2016013017281538000_exv090v1.12","doi-asserted-by":"crossref","unstructured":"A. Banerjee and D. A. Naumann. 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, 2005.","DOI":"10.1007\/978-3-540-30569-9_2"},{"key":"2016013017281538000_exv090v1.13","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.007"},{"key":"2016013017281538000_exv090v1.14","doi-asserted-by":"publisher","DOI":"10.1007\/s11787-014-0098-0"},{"key":"2016013017281538000_exv090v1.15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S1570-2464(07)80004-8","article-title":"Modal logic: a semantic perspective","volume":"3","author":"Blackburn","year":"2006","journal-title":"Handbook of Modal Logic"},{"key":"2016013017281538000_exv090v1.16","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exp041"},{"key":"2016013017281538000_exv090v1.17","first-page":"511","article-title":"A judgmental reconstruction of modal logic","volume":"11","author":"Davies","year":"2001","journal-title":"Mathematical Structures in Computer Science"},{"key":"2016013017281538000_exv090v1.18","doi-asserted-by":"crossref","unstructured":"Davies R. Pfenning F. A modal analysis of staged computation. In POPL, pp. 258\u2013270, 1996.","DOI":"10.21236\/ADA296537"},{"key":"2016013017281538000_exv090v1.19","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"2016013017281538000_exv090v1.20","unstructured":"Dijkstra E. W. . A Discipline of Programming, Vol. 4. Prentice-Hall Englewood Cliffs, 1976."},{"key":"2016013017281538000_exv090v1.21","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2013.07.011"},{"key":"2016013017281538000_exv090v1.22","doi-asserted-by":"crossref","unstructured":"H. Geuvers and G. I. Jojgov. Open proofs and open terms: a basis for interactive logic. In Computer Science Logic, 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September 22\u201325, 2002, Proceedings, Vol. 2471 of Lecture Notes in Computer Science, J. C. Bradfield, ed., pp. 537\u2013552. Springer, 2002.","DOI":"10.1007\/3-540-45793-3_36"},{"key":"2016013017281538000_exv090v1.23","first-page":"39","article-title":"Eine interpretation des intuitionistischen aussagenkalk\u00fcls","volume":"4","author":"G\u00f6del","year":"1933","journal-title":"Ergebnisse eines mathematischen Kolloquiums"},{"key":"2016013017281538000_exv090v1.24","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/978-3-540-24725-8_16","article-title":"Modal proofs as distributed programs","volume-title":"Programming Languages and Systems","volume":"2986","author":"Jia","year":"2004"},{"key":"2016013017281538000_exv090v1.25","unstructured":"S. Kramer. A logic of interactive proofs (formal theory of knowledge transfer). arXiv preprint arXiv:1201.3667, 2012."},{"key":"2016013017281538000_exv090v1.26","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.12.011"},{"key":"2016013017281538000_exv090v1.27","unstructured":"J.-J. L\u00e9vy. R\u00e9ductions correctes et optimales dans le lambda-calcul. PhD Thesis, Paris 7, 1978."},{"key":"2016013017281538000_exv090v1.28","unstructured":"Martin-L\u00f6f P. An Intuitionistic Theory of Types. Bibliopolis, 1984."},{"key":"2016013017281538000_exv090v1.29","doi-asserted-by":"crossref","unstructured":"Martini S. Masini A. Wansing H. A computational interpretation of modal proofs. In Proof Theory of Modal Logic, pp. 213\u2013241. Springer, 1996.","DOI":"10.1007\/978-94-017-2798-3_12"},{"key":"2016013017281538000_exv090v1.30","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/11506676_5","article-title":"Logical mobility and locality types","volume-title":"Logic Based Program Synthesis and Transformation","volume":"3573","author":"Moody","year":"2005"},{"key":"2016013017281538000_exv090v1.31","unstructured":"J. Moody. Modal logic as a basis for distributed computation. Technical Report CMU-CS-03-194, Carnegie Mellon University, 2003."},{"key":"2016013017281538000_exv090v1.32","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094628"},{"key":"2016013017281538000_exv090v1.33","doi-asserted-by":"crossref","unstructured":"T. Murphy, K. Crary, R. Harper, F. Pfenning et al. A symmetric modal lambda calculus for distributed computing. In Logic in Computer Science, 2004. Proceedings of the 19th Annual IEEE Symposium on, pp. 286\u2013295. IEEE, 2004.","DOI":"10.1109\/LICS.2004.1319623"},{"key":"2016013017281538000_exv090v1.34","doi-asserted-by":"publisher","DOI":"10.2307\/2268135"},{"key":"2016013017281538000_exv090v1.35","doi-asserted-by":"crossref","first-page":"23:1","DOI":"10.1145\/1352582.1352591","article-title":"Contextual modal type theory","volume":"9","author":"Nanevski","year":"2008","journal-title":"ACM Transactions on Computational Logic"},{"key":"2016013017281538000_exv090v1.36","first-page":"263","article-title":"The logic of compatibility of propositions","volume":"35","author":"Orlov","year":"1925","journal-title":"Matematicheskii Sbornik"},{"key":"2016013017281538000_exv090v1.37","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013061"},{"key":"2016013017281538000_exv090v1.38","doi-asserted-by":"publisher","DOI":"10.2307\/2275652"},{"key":"2016013017281538000_exv090v1.39","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00028-3"},{"key":"2016013017281538000_exv090v1.40","doi-asserted-by":"crossref","unstructured":"Pientka B. Blume M. Kobayashi N. Vidal G. Beluga: programming with dependent types, contextual data, and contexts. In Functional and Logic Programming, pp. 1\u201312. Springer, 2010.","DOI":"10.1007\/978-3-642-12251-4_1"},{"key":"2016013017281538000_exv090v1.41","doi-asserted-by":"crossref","unstructured":"P. V. Rangan. An axiomatic basis of trust in distributed systems. In Security and Privacy, 1988. Proceedings, 1988 IEEE Symposium on, pp. 204\u2013211. IEEE, 1988.","DOI":"10.1109\/SECPRI.1988.8112"},{"key":"2016013017281538000_exv090v1.42","doi-asserted-by":"crossref","unstructured":"A. Saurin. On the relations between the syntactic theories of lambda-mu-calculi. In Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16\u201319, 2008. Proceedings, Vol. 5213 of Lecture Notes in Computer Science, M. Kaminski and S. Martini, eds, pp. 154\u2013168. Springer, 2008.","DOI":"10.1007\/978-3-540-87531-4_13"},{"key":"2016013017281538000_exv090v1.43","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1145\/1805950.1805958","article-title":"Typing streams in the \u03bb\u03bc-calculus","volume":"11","author":"Saurin","year":"2010","journal-title":"ACM Transactions on Computational Logic (TOCL)"},{"key":"2016013017281538000_exv090v1.44","doi-asserted-by":"publisher","DOI":"10.1007\/BF02757006"},{"key":"2016013017281538000_exv090v1.45","doi-asserted-by":"crossref","unstructured":"S\u00f8rensen M. H. Urzyczyn P. Lectures on the Curry\u2013Howard isomorphism , Vol. 149 of Studies in Logic and the Foundations of Mathematics. Elsevier Science, 2006.","DOI":"10.1016\/S0049-237X(06)80005-4"},{"key":"2016013017281538000_exv090v1.46","doi-asserted-by":"crossref","unstructured":"R. E. Yavorsky. On arithmetical completeness of first-order logics of provability. In Advances in Modal Logic 3, Papers from the Third Conference on \u2018Advances in Modal logic\u2019, held in Leipzig (Germany) in October 2000, F. Wolter, H. Wansing, M. de Rijke and M. Zakharyaschev, eds, pp. 1\u201316. World Scientific, 2000.","DOI":"10.1142\/9789812776471_0001"},{"key":"2016013017281538000_exv090v1.47","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00067-7"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/27\/4\/1023\/17659896\/exv090.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T02:18:52Z","timestamp":1718331532000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article-lookup\/doi\/10.1093\/logcom\/exv090"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,30]]},"references-count":47,"alternative-id":["10.1093\/logcom\/exv090"],"URL":"https:\/\/doi.org\/10.1093\/logcom\/exv090","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,1,30]]}}}