{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214245,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540657514"},{"type":"electronic","value":"9783540489757"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48975-4_12","type":"book-chapter","created":{"date-parts":[[2007,8,9]],"date-time":"2007-08-09T18:28:27Z","timestamp":1186684107000},"page":"231-250","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Mathematical Vernacular and Conceptual Well-Formedness in Mathematical Language"],"prefix":"10.1007","author":[{"given":"Zhaohui","family":"Luo","sequence":"first","affiliation":[]},{"given":"Paul","family":"Callaghan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,5,22]]},"reference":[{"key":"12_CR1","unstructured":"A. Bailey. The Machine-checked Literate Formalisation of Algebra in Type Theory. PhD thesis, University of Manchester, 1998."},{"key":"12_CR2","unstructured":"R. Burstall and J. McKinna. Deliverables: a categorical approach to program development in type theory. LFCS report ECS-LFCS-92-242, Dept of Computer Science, University of Edinburgh, 1992."},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"A. Copestake and T. Briscoe. Semi-productive polysemy and sense extension. In J. Pustejovsky and B. Boguraev, editors, Lexical Semantics: The Problem of Polysemy. Clarendon, 1996.","DOI":"10.1093\/jos\/12.1.15"},{"key":"12_CR4","series-title":"Technical Report","volume-title":"Extractingtexts from proofs","author":"Y. Coscoy","year":"1995","unstructured":"Y. Coscoy, G. Kahn, and L. Th\u00e9ry. Extractingtexts from proofs. Technical Report 2459, INRIA, Sophia-Antipolis, 1995."},{"key":"12_CR5","unstructured":"P. Callaghan and Z. Luo. Mathematical vernacular in type theory-based proof assistants. In R. Backhouse, editor, User Interfaces for Theorem Proving, UITP '98, July 1998."},{"key":"12_CR6","unstructured":"Coq. The Coq Proof Assistant Reference Manual (version 6.1). INRIA-Rocquencourt and CNRS-ENS Lyon, 1996."},{"key":"12_CR7","unstructured":"N.G. de Bruijn. A survey of the project AUTOMATH. In J. Hindley and J. Seldin, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980."},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"N. G. de Bruijn. The mathematical vernacular, a language for mathematics with typed sets. In R. P. Nederpelt, J. H. Geuvers, and R. C. de Vrijer, editors, Selected Papers on Automath. North Holland, 1994.","DOI":"10.1016\/S0049-237X(08)70231-3"},{"key":"12_CR9","unstructured":"R. Jackendoff. The Architecture of the Language Faculty. MIT, 1997."},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"A. Jones, Z. Luo, and S. Soloviev. Some proof-theoretic and algorithmic aspects of coercive subtyping. Proc. of the Annual Conf on Types and Proofs (TYPES'96), 1997. To appear.","DOI":"10.1007\/BFb0097792"},{"key":"12_CR11","unstructured":"A. Jones. The formalization of linear algebra in LEGO: The decidable dependency theorem. Master's thesis, University of Manchester, 1995."},{"key":"12_CR12","unstructured":"Z. Luo and R. Pollack. LEGO Proof Development System: User's Manual. LFCS Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh, 1992."},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Z. Luo. A higher-order calculus and theory abstraction. Information and Computation, 90(1), 1991.","DOI":"10.1016\/0890-5401(91)90062-7"},{"key":"12_CR14","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the Fourth Inter. Joint Conf. on the Theory and Practice of Software Development (TAPSOFT)","author":"Z. Luo","year":"1991","unstructured":"Z. Luo. Program specification and data refinement in type theory. Proc. of the Fourth Inter. Joint Conf. on the Theory and Practice of Software Development (TAPSOFT), LNCS 493, 1991. Also as LFCS report ECSLFCS-91-131, Dept. of Computer Science, Edinburgh University."},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Z. Luo. Program specification and data refinement in type theory. Mathematical Structures in Computer Science, 3(3), 1993. An earlier version appears as [Luo91b].","DOI":"10.1017\/S0960129500000256"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994.","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"key":"12_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of CSL'96, the 1996 Annual Conference of the European Association for Computer Science Logic","author":"Z. Luo","year":"1997","unstructured":"Z. Luo. Coercive subtypingin type theory. Proc. of CSL'96, the 1996 Annual Conference of the European Association for Computer Science Logic, Utrecht. LNCS 1258, 1997."},{"key":"12_CR18","unstructured":"Z. Luo. Coercive subtyping. Journal of Logic and Computation, 1998. To appear."},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"J. Lyons. Linguistic Semantics. Cambridge University Press, 1995.","DOI":"10.1017\/CBO9780511810213"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"J. McKinna. Deliverables: a categorical approach to program development in type theory. PhD thesis, Department of Computer Science, University of Edinburgh, 1992.","DOI":"10.1007\/3-540-57182-5_3"},{"key":"12_CR21","unstructured":"Mizar. Mizar home page. http:\/\/mizar.uw.bialystok.pl\/ ."},{"key":"12_CR22","series-title":"Lect Notes Comput Sci","volume-title":"Types for Proof and Programs","author":"L. Magnusson","year":"1994","unstructured":"L. Magnusson and B. Nordstr\u00f6m. The ALF proof editor and its proof engine. In Types for Proof and Programs, LNCS, 1994."},{"key":"12_CR23","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J. Smith. Programming in Martin-L\u00f6f's Type Theory: An Introduction. Oxford University Press, 1990."},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"J. Pustejovsky. The Generative Lexicon. MIT, 1995.","DOI":"10.7551\/mitpress\/3225.001.0001"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"A. Ranta. Type-theoretical Grammar. Oxford University Press, 1994.","DOI":"10.1093\/oso\/9780198538578.001.0001"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"A. Ranta. Type-theoretical interpretation and generalization of phrase structure grammar. Bulletin of the IGPL, 1995.","DOI":"10.1093\/jigpal\/3.2-3.319"},{"key":"12_CR27","volume-title":"Types for Proofs and Programs","author":"A. Ranta","year":"1996","unstructured":"Aarne Ranta. Context-relative syntactic categories and the formalization of mathematical text. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs. Springer-Verlag, Heidelberg, 1996."},{"key":"12_CR28","unstructured":"A. Ranta. A grammatical framework (some notes on the source files), 1997."},{"key":"12_CR29","unstructured":"Mark Ruys. Formalizing Mathematics in Type Theory. PhD thesis, Computing Science Institute, University of Nijmegen. (to be submitted)."},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"A. Saibi. Typing algorithm in type theory with inheritance. Proc of POPL'97, 1997.","DOI":"10.1145\/263699.263742"},{"key":"12_CR31","unstructured":"S. Soloviev and Z. Luo. Coercive subtyping: coherence and conservativity, 1998. In preparation."},{"key":"12_CR32","unstructured":"L. van Benthem Jutting, James McKinna, and Robert Pollack. Type checking in pure type systems. submitted for publication, 1993."}],"container-title":["Lecture Notes in Computer Science","Logical Aspects of Computational Linguistics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48975-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T06:58:09Z","timestamp":1737356289000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48975-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540657514","9783540489757"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-48975-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"22 May 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}