{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:21:24Z","timestamp":1740122484942,"version":"3.37.3"},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2023,5,3]],"date-time":"2023-05-03T00:00:00Z","timestamp":1683072000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,5,3]],"date-time":"2023-05-03T00:00:00Z","timestamp":1683072000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100004359","name":"Swedish Research Council","doi-asserted-by":"crossref","award":["2014-39"],"award-info":[{"award-number":["2014-39"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100003819","name":"Natural Science Foundation of Hubei Province","doi-asserted-by":"publisher","award":["2019CFB742"],"award-info":[{"award-number":["2019CFB742"]}],"id":[{"id":"10.13039\/501100003819","id-type":"DOI","asserted-by":"publisher"}]},{"name":"EU research network EUTypes","award":["CA15123"],"award-info":[{"award-number":["CA15123"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J of Log Lang and Inf"],"published-print":{"date-parts":[[2023,10]]},"DOI":"10.1007\/s10849-023-09397-y","type":"journal-article","created":{"date-parts":[[2023,5,3]],"date-time":"2023-05-03T21:06:51Z","timestamp":1683148011000},"page":"733-758","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Propositional Forms of Judgemental Interpretations"],"prefix":"10.1007","volume":"32","author":[{"given":"Tao","family":"Xue","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhaohui","family":"Luo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stergios","family":"Chatzikyriakidis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,5,3]]},"reference":[{"key":"9397_CR1","unstructured":"Agda. (2008). The Agda proof assistant (version 2). Available from the web page: http:\/\/appserv.cs.chalmers.se\/users\/ulfn\/wiki\/agda.php"},{"key":"9397_CR2","volume-title":"Lexical meaning in context: a Web of Words","author":"N Asher","year":"2012","unstructured":"Asher, N. (2012). Lexical meaning in context: a Web of Words. Cambridge University Press."},{"key":"9397_CR3","doi-asserted-by":"crossref","unstructured":"Bekki, D. (2014). Representing anaphora with dependent types. LACL 2014, LNCS 8535.","DOI":"10.1007\/978-3-662-43742-1_2"},{"key":"9397_CR4","unstructured":"Bernardy, J.P. & Chatzikyriakidis, S. (2017). A type-theoretical system for the fracas test suite: Grammatical framework meets coq. In: IWCS 2017-12th International Conference on Computational Semantics-Long papers."},{"issue":"2","key":"9397_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/FI-2000-42201","volume":"42","author":"P Boldini","year":"2000","unstructured":"Boldini, P. (2000). Formalizing context in intuitionistic type theory. Fundamenta Informaticae, 42(2), 1\u201323.","journal-title":"Fundamenta Informaticae"},{"issue":"1","key":"9397_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1023\/A:1010648911114","volume":"27","author":"P Callaghan","year":"2001","unstructured":"Callaghan, P., & Luo, Z. (2001). An implementation of LF with coercive subtyping and universes. Journal of Automated Reasoning, 27(1), 3\u201327.","journal-title":"Journal of Automated Reasoning"},{"key":"9397_CR7","doi-asserted-by":"crossref","unstructured":"Chatzikyriakidis, S. & Luo, Z. (2013). Adjectives in a modern type-theoretical setting. In: Morrill G, Nederhof J (eds) Proceedings of Formal Grammar 2013. LNCS 8036, pp 159\u2013174.","DOI":"10.1007\/978-3-642-39998-5_10"},{"key":"9397_CR8","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/s10849-014-9208-x","volume":"23","author":"S Chatzikyriakidis","year":"2014","unstructured":"Chatzikyriakidis, S., & Luo, Z. (2014). Natural language reasoning in Coq. Journal of Logic, Language and Information, 23, 441\u2013480.","journal-title":"Journal of Logic, Language and Information"},{"key":"9397_CR9","doi-asserted-by":"crossref","unstructured":"Chatzikyriakidis, S., & Luo, Z. (2014). Natural language reasoning using proof-assistant technology: Rich typing and beyond. In EACL Workshop on Type Theory and Natural Language Semantics.","DOI":"10.3115\/v1\/W14-1405"},{"key":"9397_CR10","doi-asserted-by":"crossref","unstructured":"Chatzikyriakidis, S. & Luo, Z. (2016). Proof assistants for natural language semantics. In Logical Aspects of Computational Linguistics 2016, Nancy LNCS 10054","DOI":"10.1007\/978-3-662-53826-5_6"},{"issue":"1","key":"9397_CR11","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s10849-017-9246-2","volume":"26","author":"S Chatzikyriakidis","year":"2017","unstructured":"Chatzikyriakidis, S., & Luo, Z. (2017). Adjectival and adverbial modification: The view from modern type theories. Journal of Logic, Language and Information, 26(1), 45\u201388.","journal-title":"Journal of Logic, Language and Information"},{"key":"9397_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-50422-3","volume-title":"Modern perspectives in type-theoretical semantics","author":"S Chatzikyriakidis","year":"2017","unstructured":"Chatzikyriakidis, S., & Luo, Z. (2017). On the interpretation of common nouns: Types v.s. predicates. Modern perspectives in type-theoretical semantics. Springer."},{"key":"9397_CR13","volume-title":"Formal semantics in modern type theories","author":"S Chatzikyriakidis","year":"2020","unstructured":"Chatzikyriakidis, S., & Luo, Z. (2020). Formal semantics in modern type theories. Wiley."},{"issue":"1","key":"9397_CR14","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A. (1940). A formulation of the simple theory of types. Journal of Symbolic Logic, 5(1), 56\u201368.","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"9397_CR15","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1093\/logcom\/exi004","volume":"15","author":"R Cooper","year":"2005","unstructured":"Cooper, R. (2005). Records and record types in semantic theory. Journal of Logic and Compututation, 15(2), 99\u2013112.","journal-title":"Journal of Logic and Compututation"},{"key":"9397_CR16","unstructured":"Coq. (2010). The Coq Proof Assistant Reference Manual (Version 8.3), INRIA. The Coq Development Team"},{"key":"9397_CR17","volume-title":"Combinatory logic","author":"H Curry","year":"1958","unstructured":"Curry, H., & Feys, R. (1958). Combinatory logic (Vol. 1). North Holland Publishing Company."},{"issue":"4","key":"9397_CR18","doi-asserted-by":"publisher","first-page":"293","DOI":"10.3233\/FI-2010-351","volume":"104","author":"R Dapoigny","year":"2009","unstructured":"Dapoigny, R., & Barlatier, P. (2009). Modeling contexts with dependent types. Fundamenta Informaticae, 104(4), 293\u2013327.","journal-title":"Fundamenta Informaticae"},{"key":"9397_CR19","volume-title":"Intensional and higher-order modal logic: with applications to Montague semantics","author":"D Gallin","year":"1975","unstructured":"Gallin, D. (1975). Intensional and higher-order modal logic: with applications to Montague semantics. North-Holland."},{"key":"9397_CR20","unstructured":"Groenendijk, J. & Stokhof, M. (1990). Dynamic Montague grammar. In Proceedings of the second symposium on logic and language."},{"issue":"1","key":"9397_CR21","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00628304","volume":"14","author":"J Groenendijk","year":"1991","unstructured":"Groenendijk, J., & Stokhof, M. (1991). Dynamic predicate logic. Linguistics and Philosophy, 14(1), 39.","journal-title":"Linguistics and Philosophy"},{"key":"9397_CR22","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L Henkin","year":"1950","unstructured":"Henkin, L. (1950). Completeness in the theory of types. Journal of Symbolic Logic, 15, 81\u201391.","journal-title":"Journal of Symbolic Logic"},{"key":"9397_CR23","unstructured":"Howard, W. (1980). The formulae-as-types notion of construction. In: Hindley J, Seldin J (eds) To H. B. Curry: Essays on Combinatory Logic, Academic Press, (Notes written and distributed in 1969.)"},{"key":"9397_CR24","unstructured":"Kahle, R. & Schroeder-Heister, P. (eds) (2006). Proof-theoretic semantics. special issue of synthese."},{"key":"9397_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-1616-1","volume-title":"From discourse to logic","author":"H Kamp","year":"1993","unstructured":"Kamp, H., & Reyle, U. (1993). From discourse to logic. Kluwer."},{"key":"9397_CR26","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538356.001.0001","volume-title":"Computation and reasoning: A type theory for computer science","author":"Z Luo","year":"1994","unstructured":"Luo, Z. (1994). Computation and reasoning: A type theory for computer science. Oxford University Press."},{"issue":"1","key":"9397_CR27","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1093\/logcom\/9.1.105","volume":"9","author":"Z Luo","year":"1999","unstructured":"Luo, Z. (1999). Coercive subtyping. Journal of Logic and Computation, 9(1), 105\u2013130.","journal-title":"Journal of Logic and Computation"},{"key":"9397_CR28","doi-asserted-by":"crossref","unstructured":"Luo, Z. (2009). Type-theoretical semantics with coercive subtyping. Semantics and Linguistic Theory 20 (SALT20), Vancouver","DOI":"10.3765\/salt.v20i0.2580"},{"key":"9397_CR29","doi-asserted-by":"crossref","unstructured":"Luo, Z. (2011). Contextual analysis of word meanings in type-theoretical semantics. Logical Aspects of Computational Linguistics (LACL\u20192011) LNAI 6736","DOI":"10.1007\/978-3-642-22221-4_11"},{"key":"9397_CR30","doi-asserted-by":"crossref","unstructured":"Luo, Z. (2012). Common nouns as types. In: Bechet D, Dikovsky A (eds) Logical Aspects of Computational Linguistics (LACL\u20192012). LNCS 7351, pp 173\u2013185","DOI":"10.1007\/978-3-642-31262-5_12"},{"issue":"6","key":"9397_CR31","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/s10988-013-9126-4","volume":"35","author":"Z Luo","year":"2012","unstructured":"Luo, Z. (2012). Formal semantics in modern type theories with coercive subtyping. Linguistics and Philosophy, 35(6), 491\u2013513.","journal-title":"Linguistics and Philosophy"},{"key":"9397_CR32","doi-asserted-by":"crossref","unstructured":"Luo, Z. (2014). Formal semantics in modern type theories: Is it model-theoretic, proof-theoretic, or both? In: Invited talk at logical aspects of computational linguistics 2014 (LACL 2014). Toulouse LNCS, 8535, 177\u2013188.","DOI":"10.1007\/978-3-662-43742-1_14"},{"key":"9397_CR33","unstructured":"Luo, Z. (2018). Formal semantics in modern type theories (and event semantics in mtt-framework). In: Invited talk at LACompLing18"},{"key":"9397_CR34","unstructured":"Luo, Z. (2019). Formal Semantics in Modern Type Theories (MTT-semantics is both model\/proof-theoretic). Proof-Theoretic Semantics: Assessment and Future Perspectives, In: Proceedings of the Third Tuebingen Conference on Proof-Theoretic Semantics, Tuebingen"},{"key":"9397_CR35","doi-asserted-by":"crossref","unstructured":"Luo, Z. (2019). Proof irrelevance in type-theoretical semantics. Logic and Algorithms in Computational Linguistics 2018 (LACompLing2018), Studies in Computational Intelligence (SCI) Springer","DOI":"10.1007\/978-3-030-30077-7_1"},{"key":"9397_CR36","unstructured":"Luo, Z. & Callaghan, P. (1998). Coercive subtyping and lexical semantics (extended abstract). In: Logical Aspects of Computational Linguistics (LACL\u201998)."},{"key":"9397_CR37","unstructured":"Luo, Z. & Pollack, R. (1992). LEGO Proof Development System: User\u2019s Manual. LFCS Report ECS-LFCS-92-211, Deptartment of Computer Science, University of Edinburgh"},{"key":"9397_CR38","unstructured":"Luo, Z. & Xue, T. (2020). Disjointness of types and negative occurrences. Notes, February 2020."},{"key":"9397_CR39","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1016\/j.ic.2012.10.020","volume":"223","author":"Z Luo","year":"2013","unstructured":"Luo, Z., Soloviev, S., & Xue, T. (2013). Coercive subtyping: theory and implementation. Information and Computation, 223, 18\u201342.","journal-title":"Information and Computation"},{"key":"9397_CR40","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P. (1975). An intuitionistic theory of types: predicative part. In: HRose, JCShepherdson (eds) Logic Colloquium\u201973.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"9397_CR41","unstructured":"McBride, C. (2002). Elimination with a motive. In: Callaghan P, Luo Z, McKinna J, Pollack R (eds) Types for Proofs and Programs, In: Proceedings of TYPES 2000, LNCS 2277, Springer"},{"issue":"1","key":"9397_CR42","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1017\/S0956796803004829","volume":"14","author":"C McBride","year":"2004","unstructured":"McBride, C., & McKinna, J. (2004). The view from the left. Journal of Functional Programming, 14(1), 69\u2013111.","journal-title":"Journal of Functional Programming"},{"key":"9397_CR43","doi-asserted-by":"crossref","unstructured":"Mineshima, K., Mart\u00ednez-G\u00f3mez, P., Miyao, Y. & Bekki, D. (2015). Higher-order logical inference with compositional semantics. In: Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing, pp 2055\u20132061","DOI":"10.18653\/v1\/D15-1244"},{"key":"9397_CR44","volume-title":"Untersuchungen zu einer konstruktiven Semantik fur ein Fragment des Englischen","author":"U M\u00f6nnich","year":"1985","unstructured":"M\u00f6nnich, U. (1985). Untersuchungen zu einer konstruktiven Semantik fur ein Fragment des Englischen. University of T\u00fcbingen."},{"key":"9397_CR45","volume-title":"Formal philosophy: Selected papers of Richard Montague","author":"R Montague","year":"1974","unstructured":"Montague, R. (1974). Formal philosophy: Selected papers of Richard Montague. Yale University Press."},{"issue":"2","key":"9397_CR46","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/BF00635836","volume":"19","author":"R Muskens","year":"1996","unstructured":"Muskens, R. (1996). Combining Montague semantics and discourse representation. Linguistics and Philosophy, 19(2), 143\u2013186.","journal-title":"Linguistics and Philosophy"},{"key":"9397_CR47","volume-title":"Programming in martin-L\u00f6f\u2019s type theory: An introduction","author":"B Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., & Smith, J. (1990). Programming in martin-L\u00f6f\u2019s type theory: An introduction. Oxford University Press."},{"key":"9397_CR48","volume-title":"Type-theoretical grammar","author":"A Ranta","year":"1994","unstructured":"Ranta, A. (1994). Type-theoretical grammar. Oxford University Press."},{"key":"9397_CR49","unstructured":"Retor\u00e9, C. (2014). The Montagovian Generative Lexicon Ty$$_n$$: a type theoretical framework for natural language semantics. In: proofs and programs (TYPES 2013), LIPIcs(26)."},{"key":"9397_CR50","doi-asserted-by":"crossref","unstructured":"Sundholm, G. (1986). Proof theory and meaning. D Gabbay and F Guenthner (eds) In: Handbook of Philosophical Logic, Vol III.","DOI":"10.1007\/978-94-009-5203-4_8"},{"issue":"1","key":"9397_CR51","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00873254","volume":"79","author":"G Sundholm","year":"1989","unstructured":"Sundholm, G. (1989). Constructive generalized quantifiers. Synthese, 79(1), 1\u201312.","journal-title":"Synthese"},{"key":"9397_CR52","unstructured":"Xue, T. (2013). Theory and implementation of coercive subtyping. PhD thesis, Royal Holloway, University of London"},{"key":"9397_CR53","doi-asserted-by":"crossref","unstructured":"Xue, T. & Luo, Z. (2012). Dot-types and their implementation. In: Logical aspects of computational linguistics (LACL 2012) LNCS 7351.","DOI":"10.1007\/978-3-642-31262-5_17"},{"key":"9397_CR54","doi-asserted-by":"crossref","unstructured":"Xue, T., Luo, Z. & Chatzikyriakidis, S. (2018). Propositional forms of judgemental interpretations. In: Proceedings of workshop on natural language and computer science oxford","DOI":"10.29007\/kv25"}],"container-title":["Journal of Logic, Language and Information"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10849-023-09397-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10849-023-09397-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10849-023-09397-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,12]],"date-time":"2023-12-12T00:35:18Z","timestamp":1702341318000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10849-023-09397-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,3]]},"references-count":54,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,10]]}},"alternative-id":["9397"],"URL":"https:\/\/doi.org\/10.1007\/s10849-023-09397-y","relation":{},"ISSN":["0925-8531","1572-9583"],"issn-type":[{"type":"print","value":"0925-8531"},{"type":"electronic","value":"1572-9583"}],"subject":[],"published":{"date-parts":[[2023,5,3]]},"assertion":[{"value":"1 April 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 May 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}