{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T06:12:46Z","timestamp":1725862366127},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662529201"},{"type":"electronic","value":"9783662529218"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-662-52921-8_20","type":"book-chapter","created":{"date-parts":[[2016,8,5]],"date-time":"2016-08-05T11:22:30Z","timestamp":1470396150000},"page":"316-337","source":"Crossref","is-referenced-by-count":0,"title":["A Curry\u2013Howard View of Basic Justification Logic"],"prefix":"10.1007","author":[{"given":"Konstantinos","family":"Pouliasis","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,8,6]]},"reference":[{"issue":"1","key":"20_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2687821","volume":"7","author":"S Artemov","year":"2001","unstructured":"Artemov, S.: Explicit provability and constructive semantics. Bull. Symbolic Logic 7(1), 1\u201336 (2001)","journal-title":"Bull. Symbolic Logic"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1007\/978-3-540-72734-7_2","volume-title":"Logical Foundations of Computer Science","author":"S Artemov","year":"2007","unstructured":"Artemov, S., Bonelli, E.: The intensional lambda calculus. In: Artemov, S., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 12\u201325. Springer, Heidelberg (2007)"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Bavera, F., Bonelli, E.: Justification logic and audited computation. J. Logic Comput., p. exv037 (2015)","DOI":"10.1093\/logcom\/exv037"},{"key":"20_CR4","unstructured":"Bellin, G., de Paiva, V.C., Ritter, E.: Extended curry-howard correspondence for a basic constructive modal logic (2001). (preprint; presented at M4M\u20132, ILLC, UvAmsterdam)"},{"issue":"3","key":"20_CR5","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1023\/A:1005291931660","volume":"65","author":"GM Bierman","year":"2000","unstructured":"Bierman, G.M., de Paiva, V.C.V.: On an intuitionistic modal logic. Stud. Logica 65(3), 383\u2013416 (2000)","journal-title":"Stud. Logica"},{"issue":"1","key":"20_CR6","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische schlie\u00dfen I. Math. Z. 39(1), 176\u2013210 (1935)","journal-title":"Math. Z."},{"key":"20_CR7","volume-title":"Proofs and Types","author":"JY Girard","year":"1989","unstructured":"Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, New York (1989). ISBN 0-521-37181-3"},{"issue":"1","key":"20_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J-Y Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50(1), 1\u2013101 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR9","unstructured":"Kavvos, A.: System k: a simple modal $$\\lambda $$ -calculus. arXiv preprint arXiv:1602.04860 (2016)"},{"issue":"4","key":"20_CR10","first-page":"287","volume":"2","author":"J Lambek","year":"1968","unstructured":"Lambek, J.: Deductive systems and categories. Theory Comput. Syst. 2(4), 287\u2013318 (1968)","journal-title":"Theory Comput. Syst."},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Lambek, J.: Deductive systems and categories II. standard constructions and closed categories. In: Category Theory, Homology Theory and Their Applications I, pp. 76\u2013122. Springer, New York (1969)","DOI":"10.1007\/BFb0079385"},{"issue":"04","key":"20_CR12","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(04), 511\u2013540 (2001). ISSN 0960\u20131295","journal-title":"Math. Struct. Comput. Sci."},{"key":"20_CR13","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/j.entcs.2013.12.012","volume":"300","author":"K Pouliasis","year":"2014","unstructured":"Pouliasis, K., Primiero, G.: J-calc: a typed lambda calculus for intuitionistic justification logic. Electron. Notes Theor. Comput. Sci. 300, 71\u201387 (2014). ISSN 1571\u20130661","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"20_CR14","volume-title":"Natural Deduction: A Proof-Theoretical study","author":"D Prawitz","year":"1965","unstructured":"Prawitz, D.: Natural Deduction: A Proof-Theoretical study. Almquist & Wiksell, Stockholm (1965)"},{"key":"20_CR15","volume-title":"Constructivism in Mathematics: An Introduction","author":"AS Troelstra","year":"1988","unstructured":"Troelstra, A.S., Van Dalen, D.: Constructivism in Mathematics: An Introduction. North-Holland, Amsterdam (1988)"},{"key":"20_CR16","unstructured":"Pfenning, F.: Automated theorem proving (2004). http:\/\/www.cs.cmu.edu\/~fp\/courses\/atp\/handouts\/atp.pdf"},{"issue":"1","key":"20_CR17","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1023\/A:1005091418752","volume":"60","author":"W Sieg","year":"1998","unstructured":"Sieg, W., Byrnes, J.: Normal natural deduction proofs (in classical logic). Stud. Logica 60(1), 67\u2013106 (1998)","journal-title":"Stud. Logica"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, Information, and Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-52921-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T16:04:04Z","timestamp":1498320244000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-52921-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662529201","9783662529218"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-52921-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}