{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T12:30:29Z","timestamp":1725798629802},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662445211"},{"type":"electronic","value":"9783662445228"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-44522-8_28","type":"book-chapter","created":{"date-parts":[[2014,8,12]],"date-time":"2014-08-12T10:12:23Z","timestamp":1407838343000},"page":"327-339","source":"Crossref","is-referenced-by-count":1,"title":["L ax F: Side Conditions and External Evidence as Monads"],"prefix":"10.1007","author":[{"given":"Furio","family":"Honsell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luigi","family":"Liquori","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ivan","family":"Scagnetto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"28_CR1","unstructured":"Albert, H.: Traktat \u00fcber kritische Vernunft. J.C.B. Mohr (Paul Siebeckggu), T\u00fcbingen (1991)"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Alechina, N., Mendler, M., de Paiva, V., Ritter, E.: Categorical and Kripke Semantics for Constructive S4 Modal Logic. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol.\u00a02142, pp. 292\u2013307. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-44802-0_21"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"Baillot, P., Coppola, P., Lago, U.D.: Light logics and optimal reduction: Completeness and complexity. In: Proc. LICS, pp. 421\u2013430. IEEE Computer Society (2007)","DOI":"10.1109\/LICS.2007.27"},{"key":"28_CR4","unstructured":"Barendregt, H.: Lambda Calculus: Its Syntax and Semantics. North Holland (1984)"},{"key":"28_CR5","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1023\/A:1015761529444","volume":"28","author":"H. Barendregt","year":"2002","unstructured":"Barendregt, H., Barendsen, E.: Autarkic computations in formal proofs. Journal of Automated Reasoning\u00a028, 321\u2013336 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Barthe, G., Cirstea, H., Kirchner, C., Liquori, L.: Pure Pattern Type Systems. In: Proc. POPL 2003, pp. 250\u2013261. The ACM Press (2003)","DOI":"10.1145\/640128.604152"},{"key":"28_CR7","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1093\/mind\/IV.14.278","volume":"4","author":"L. Carroll","year":"1895","unstructured":"Carroll, L.: What the Tortoise Said to Achilles. Mind\u00a04, 278\u2013280 (1895)","journal-title":"Mind"},{"key":"28_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-73228-0_9","volume-title":"Typed Lambda Calculi and Applications","author":"D. Cousineau","year":"2007","unstructured":"Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-Pi-calculus modulo. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol.\u00a04583, pp. 102\u2013117. Springer, Heidelberg (2007)"},{"issue":"1","key":"28_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1997.2627","volume":"137","author":"M. Fairtlough","year":"1997","unstructured":"Fairtlough, M., Mendler, M.: Propositional lax logic. Information and Computation\u00a0137(1), 1\u201333 (1997)","journal-title":"Information and Computation"},{"key":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/3-540-44755-5_15","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Fairtlough","year":"2001","unstructured":"Fairtlough, M., Mendler, M., Cheng, X.: Abstraction and refinement in higher-order logic. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 201\u2013216. Springer, Heidelberg (2001)"},{"key":"28_CR11","unstructured":"Fairtlough, M., Mendler, M., Walton, M.: First-order Lax Logic as a Framework for Constraint Logic Programming. Tech. Rep., University of Passau (1997)"},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"Garg, D., Tschantz, M.C.: From indexed lax logic to intuitionistic logic. Tech. Rep., DTIC Document (2008)","DOI":"10.21236\/ADA476728"},{"issue":"1","key":"28_CR13","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the ACM\u00a040(1), 143\u2013184 (1993)","journal-title":"Journal of the ACM"},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BFb0028392","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Hirschkoff","year":"1997","unstructured":"Hirschkoff, D.: A full formalisation of \u03c0-calculus theory in the calculus of constructions. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 153\u2013169. Springer, Heidelberg (1997)"},{"key":"28_CR15","first-page":"37","volume-title":"Proc. LFMTP 2013","author":"F. Honsell","year":"2013","unstructured":"Honsell, F.: 25 years of formal proof cultures: Some problems, some philosophy, bright future. In: Proc. LFMTP 2013, pp. 37\u201342. ACM, New York (2013)"},{"issue":"1","key":"28_CR16","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S0304-3975(98)00140-6","volume":"212","author":"F. Honsell","year":"1999","unstructured":"Honsell, F., Lenisa, M.: Semantical analysis of perpetual strategies in \u03bb-calculus. Theoretical Computer Science\u00a0212(1), 183\u2013209 (1999)","journal-title":"Theoretical Computer Science"},{"key":"28_CR17","first-page":"399","volume":"172","author":"F. Honsell","year":"2007","unstructured":"Honsell, F., Lenisa, M., Liquori, L.: A Framework for Defining Logical Frameworks. v. in Honor of G. Plotkin. ENTCS\u00a0172, 399\u2013436 (2007)","journal-title":"ENTCS"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Honsell, F., Lenisa, M., Liquori, L., Maksimovic, P., Scagnetto, I.: An Open Logical Framework. Journal of Logic and Computation (October 2013)","DOI":"10.1093\/logcom\/ext028"},{"key":"28_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-540-89439-1_10","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F. Honsell","year":"2008","unstructured":"Honsell, F., Lenisa, M., Goel, G., Scagnetto, I.: A Conditional Logical Framework. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 143\u2013157. Springer, Heidelberg (2008)"},{"issue":"2","key":"28_CR20","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/S0304-3975(00)00095-5","volume":"253","author":"F. Honsell","year":"2001","unstructured":"Honsell, F., Miculan, M., Scagnetto, I.: \u03c0-calculus in (Co)Inductive Type Theories. Theoretical Computer Science\u00a0253(2), 239\u2013285 (2001)","journal-title":"Theoretical Computer Science"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"Mendler, M.: Constrained proofs: A logic for dealing with behavioral constraints in formal hardware verification. In: Proc. Designing Correct Circuits, pp. 1\u201328. Springer (1991)","DOI":"10.1007\/978-1-4471-3544-9_1"},{"key":"28_CR22","unstructured":"Moggi, E.: The partial lambda calculus. PhD thesis, University of Edinburgh. College of Science and Engineering. School of Informatics (1988)"},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Pfenning, F., Pientka, B.: Contextual Modal Type Theory. ACM Transactions on Computational Logic 9(3) (2008)","DOI":"10.1145\/1352582.1352591"},{"key":"28_CR24","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf \u2013 a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"28_CR25","doi-asserted-by":"crossref","unstructured":"Pientka, B., Dunfield, J.: Programming with proofs and explicit contexts. In: Proc. PPDP 2008, pp. 163\u2013173. ACM (2008)","DOI":"10.1145\/1389449.1389469"},{"key":"28_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-14203-1_2","volume-title":"Automated Reasoning","author":"B. Pientka","year":"2010","unstructured":"Pientka, B., Dunfield, J.: Beluga: A framework for programming and reasoning with deductive systems (system description). In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 15\u201321. Springer, Heidelberg (2010)"},{"key":"28_CR27","doi-asserted-by":"crossref","unstructured":"Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A Concurrent Logical Framework I: Judgments and Properties. Tech. Rep. CMU-CS-02-101, CMU (2002)","DOI":"10.21236\/ADA418517"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-44522-8_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T15:02:40Z","timestamp":1558969360000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-44522-8_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662445211","9783662445228"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-44522-8_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}