{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T11:10:02Z","timestamp":1749726602622,"version":"3.41.0"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1998,7,1]],"date-time":"1998-07-01T00:00:00Z","timestamp":899251200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,7,1]],"date-time":"1998-07-01T00:00:00Z","timestamp":899251200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Logic, Language and Information"],"published-print":{"date-parts":[[1998,7]]},"DOI":"10.1023\/a:1008254612284","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T13:47:34Z","timestamp":1040564854000},"page":"265-296","source":"Crossref","is-referenced-by-count":8,"title":["Modal Pure Type Systems"],"prefix":"10.1007","volume":"7","author":[{"given":"Tijn","family":"Borghuis","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"140820_CR1","first-page":"1","volume-title":"Types for Proofs and Programs: Selected Papers International Workshop TYPES '94","author":"R. Ahn","year":"1994","unstructured":"Ahn, R., 1994, \u201cCommunicating contexts: A pragmatic approach to information change,\u201d pp. 1\u201313 in Types for Proofs and Programs: Selected Papers International Workshop TYPES '94, P. Dybjer, B. Nordstr\u00f6m, and J. Smith, eds., Berlin: Springer-Verlag."},{"key":"140820_CR2","volume-title":"Papers from the Second Symposium on Logic and Language","author":"R. Ahn","year":"1990","unstructured":"Ahn, R. and Kolb, H.P., 1990, \u201cDiscourse representation meets constructive mathematics,\u201d in Papers from the Second Symposium on Logic and Language, L. K\u00e1lm\u00e1n and L. P\u00f3l\u00f3s, eds., Budapest: Akad\u00e9mia Kiad\u00f3."},{"key":"140820_CR3","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1007\/BF00849729","volume":"8","author":"R.M.C. Ahn","year":"1994","unstructured":"Ahn, R.M.C., Beun, R.J., Borghuis, T., Bunt, H.C., and van Overveld, C.W.A.M., 1994, \u201cThe DenKarchitecture: A fundamental approach to user interfaces,\u201d Artificial Intelligence Review\n8, 431\u2013455.","journal-title":"Artificial Intelligence Review"},{"key":"140820_CR4","first-page":"117","volume-title":"Handbook of Logic in Computer Science","author":"H. Barendregt","year":"1992","unstructured":"Barendregt, H., 1992, \u201cLambda calculi with types,\u201d pp. 117\u2013309 in Handbook of Logic in Computer Science, A. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, eds., Oxford: Oxford University Press."},{"key":"140820_CR5","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"European Symposium on Programming","author":"H. Barendregt","year":"1990","unstructured":"Barendregt, H. and Hemerik, K., 1990, \u201cTypes in lambda calculus and programming languages,\u201d pp. 1\u201336 in European Symposium on Programming, N. Jones, ed., Lecture Notes in Computer Science, Vol. 432, Berlin: Springer-Verlag."},{"key":"140820_CR6","first-page":"5","volume":"133\u2013134","author":"J. Van Benthem","year":"1991","unstructured":"Van Benthem, J., 1991, \u201cReflections on epistemic logic,\u201d Logique & Analyse\n133\u2013134, 5\u201314.","journal-title":"Logique & Analyse"},{"key":"140820_CR7","unstructured":"Van Benthem Jutting, L.S., 1977, \u201cChecking Landau's \u2018Grundlagen\u2019 in the Automath system,\u201d Ph.D. Thesis, Eindhoven University of Technology."},{"key":"140820_CR8","volume-title":"Towards a mathematical analysis of the Coquand\u2014Huet calculus of constructions and the other systems in Barendregt's cube","author":"S. Berardi","year":"1988","unstructured":"Berardi, S., 1988, \u201cTowards a mathematical analysis of the Coquand\u2014Huet calculus of constructions and the other systems in Barendregt's cube,\u201d Department of Computer Science, Carnegie-Mellon University and Dipartimento Matematica, Unversit\u00e0 di Torino, Italy."},{"key":"140820_CR9","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/978-94-015-8242-1_3","volume-title":"Diamonds and Defaults","author":"T. Borghuis","year":"1993","unstructured":"Borghuis, T., 1993, \u201cInterpreting modal natural deduction in type theory,\u201d pp. 67\u2013102 in Diamonds and Defaults, M. De Rijke, ed., Dordrecht: Kluwer Academic Publishers."},{"key":"140820_CR10","unstructured":"Borghuis, T., 1994, \u201cComing to terms with modal logic: On the interpretation of modalities in typed lambda calculus,\u201d Ph.D. Thesis, Eindhoven University of Technology."},{"key":"140820_CR11","first-page":"37","volume-title":"Proceedings of the International Conference on Cooperative Multimodal Communication CMC\/95","author":"T. Borghuis","year":"1995","unstructured":"Borghuis, T., 1995, \u201cContexts in dialogue,\u201d pp. 37\u201348 in Proceedings of the International Conference on Cooperative Multimodal Communication CMC\/95, H. Bunt, R.\u2014J. Beun, and T. Borghuis, eds., Tilburg: Samenwerkings Orgaan Brabantse Universiteiten."},{"key":"140820_CR12","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511621192","volume-title":"Modal Logic: An Introduction","author":"B.F. Chellas","year":"1980","unstructured":"Chellas, B.F., 1980, Modal Logic: An Introduction, Cambridge: Cambridge University Press."},{"key":"140820_CR13","volume-title":"Symbolic Logic, An Introduction","author":"F.B. Fitch","year":"1952","unstructured":"Fitch, F.B., 1952, Symbolic Logic, An Introduction, New York: The Ronald Press Company."},{"key":"140820_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logics","author":"M. Fitting","year":"1983","unstructured":"Fitting, M., 1983, Proof Methods for Modal and Intuitionistic Logics, Dordrecht: Reidel Publishing Company."},{"key":"140820_CR15","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538332.001.0001","volume-title":"Labeled Deductive Systems","author":"D.M. Gabbay","year":"1996","unstructured":"Gabbay, D.M., 1996, Labeled Deductive Systems, Oxford: Clarendon Press."},{"key":"140820_CR16","unstructured":"Geuvers, H., 1993, \u201cLogics and type systems,\u201d Ph.D. Thesis, University of Nijmegen."},{"issue":"2","key":"140820_CR17","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"Geuvers, H. and Nederhof, M.\u2014J., 1991, \u201cModular proof of strong normalization for the calculus of constructions,\u201d Journal of Functional Programming\n1(2), 155\u2013189.","journal-title":"Journal of Functional Programming"},{"key":"140820_CR18","volume-title":"Knowledge and Belief. An Introduction to the Logic of the Two Notions","author":"J. Hintikka","year":"1962","unstructured":"Hintikka, J., 1962, Knowledge and Belief. An Introduction to the Logic of the Two Notions, Ithaca, NY: Cornell University Press."},{"key":"140820_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/3-540-16761-7_68","volume-title":"Proceedings ICALP 1986","author":"S. Kraus","year":"1986","unstructured":"Kraus, S. and Lehmann, D., 1986, \u201cKnowledge, belief and time,\u201d pp. 186\u2013195 in Proceedings ICALP 1986, L. Kott, ed., Lecture Notes in Computer Science, Vol. 226, Berlin: Springer-Verlag."},{"key":"140820_CR20","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/978-94-017-2798-3_12","volume-title":"Proof Theory of Modal Logic","author":"S. Martini","year":"1996","unstructured":"Martini, S. and Masini, A., 1996, \u201cA computational interpretation of modal proofs,\u201d pp. 213\u2013241 in Proof Theory of Modal Logic, H. Wansing, ed., Dordrecht: Kluwer Academic Publishers."},{"key":"140820_CR21","first-page":"115","volume-title":"Symposium: Set Theory, Foundations of Mathematics","author":"R.P. Nederpelt","year":"1977","unstructured":"Nederpelt, R.P., 1977, \u201cPresentation of natural deduction,\u201d pp. 115\u2013125 in Symposium: Set Theory, Foundations of Mathematics, Recueil des Travaux de l'Institut Math\u00e9matique, Nouv. s\u00e9rie, tome 2 (10), Beograd: Faculty of Mathematics, University of Beograd."},{"key":"140820_CR22","first-page":"367","volume-title":"Proceedings CSN 1990","author":"R.P. Nederpelt","year":"1990","unstructured":"Nederpelt, R.P., 1990, \u201cType systems \u2014 Basic ideas and applications,\u201d pp. 367\u2013384 in Proceedings CSN 1990, A.J. van de Goor, ed., Amsterdam: CWI."},{"issue":"4","key":"140820_CR23","doi-asserted-by":"crossref","first-page":"1319","DOI":"10.2307\/2275370","volume":"57","author":"R.J.G.B. De Queiroz","year":"1992","unstructured":"De Queiroz, R.J.G.B. and Gabbay, D.M., 1992, \u201cExtending the Curry\u2014Howard interpretation to linear, relevant and other resource logics,\u201d Journal of Symbolic Logic\n57(4), 1319\u20131365.","journal-title":"Journal of Symbolic Logic"},{"key":"140820_CR24","volume-title":"Advances in Intensional Logic","author":"R.J.G.B. De Queiroz","year":"1995","unstructured":"De Queiroz, R.J.G.B. and Gabbay, D.M., 1995, \u201cThe functional interpretation of modal necessity,\u201d in Advances in Intensional Logic, M. De Rijke, ed., Dordrecht: Kluwer Academic Publishers."},{"key":"140820_CR25","unstructured":"Thijsse, E.C.G., 1992, \u201cPartial logic and knowledge representation,\u201d Ph.D. Thesis, Tilburg, Eburon Delft."},{"key":"140820_CR26","volume-title":"LOGICA: Een Inleiding met Toepassingen in de Informatica","author":"S.C. Van Westrhenen","year":"1993","unstructured":"Van Westrhenen, S.C., Sommerhalder, R., and Tonino, J.F.M., 1993, LOGICA: Een Inleiding met Toepassingen in de Informatica, Schoonhoven: Academic Service."}],"container-title":["Journal of Logic, Language and Information"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008254612284.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008254612284\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008254612284.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T10:30:54Z","timestamp":1749724254000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008254612284"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,7]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1998,7]]}},"alternative-id":["140820"],"URL":"https:\/\/doi.org\/10.1023\/a:1008254612284","relation":{},"ISSN":["0925-8531","1572-9583"],"issn-type":[{"type":"print","value":"0925-8531"},{"type":"electronic","value":"1572-9583"}],"subject":[],"published":{"date-parts":[[1998,7]]}}}