{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T19:25:26Z","timestamp":1774639526460,"version":"3.50.1"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2001,7,1]],"date-time":"2001-07-01T00:00:00Z","timestamp":993945600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,7,1]],"date-time":"2001-07-01T00:00:00Z","timestamp":993945600000},"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 Automated Reasoning"],"published-print":{"date-parts":[[2001,7]]},"DOI":"10.1023\/a:1010648911114","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T03:31:49Z","timestamp":1040614309000},"page":"3-27","source":"Crossref","is-referenced-by-count":28,"title":["An Implementation of LF with Coercive Subtyping & Universes"],"prefix":"10.1007","volume":"27","author":[{"given":"Paul","family":"Callaghan","sequence":"first","affiliation":[]},{"given":"Zhaohui","family":"Luo","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"334552_CR1","unstructured":"Aspinall, D.: Proof General WWWsite, http:\/\/www.proofgeneral.org."},{"key":"334552_CR2","unstructured":"Bailey, A.: The machine-checked literate formalisation of algebra in type theory, Ph.D. Thesis, University of Manchester, 1998."},{"key":"334552_CR3","unstructured":"Barthe, G. and Sorensen, M. H.: Domain-free pure type systems, J. Functional Programming (to appear)."},{"key":"334552_CR4","unstructured":"Callaghan, P.: Plastic: An implementation of typed LF with coercions, Talk given in the Annual Conf. of TYPES'99, 1999."},{"key":"334552_CR5","unstructured":"Callaghan, P.: Coherence checking of coercions in Plastic, in Proc. Workshop on Subtyping & Dependent Types in Programming, 2000."},{"key":"334552_CR6","unstructured":"Callaghan, P. and Luo, Z.: Mathematical vernacular in type theory based proof assistants, in User Interfaces for Theorem Provers (UITP'98), Eindhoven, 1998."},{"key":"334552_CR7","doi-asserted-by":"crossref","unstructured":"Callaghan, P. and Luo, Z.: Implementation techniques for inductive types in Plastic, in Proc. TYPES'99, 2000.","DOI":"10.1007\/3-540-44557-9_6"},{"key":"334552_CR8","unstructured":"Coq. Coq WWWpage, http:\/\/pauillac.inria.fr\/coq."},{"key":"334552_CR9","unstructured":"Coquand, C. Adga WWWpage, http:\/\/www.cs.chalmers.se\/~catarina\/agda\/."},{"key":"334552_CR10","unstructured":"Coquand, C. and Coquand, T.: Structured type theory, in Proc. Workshop on Logical Frameworks and Meta-languages (LFM'99), 1999."},{"key":"334552_CR11","doi-asserted-by":"crossref","unstructured":"Coquand, T.: An algorithm for testing conversion in type theory, in G. Huet and G. Plotkin (eds.), Logical Frameworks, 1991.","DOI":"10.1017\/CBO9780511569807.011"},{"key":"334552_CR12","doi-asserted-by":"crossref","unstructured":"Coquand, T. and Paulin-Mohring, C.: Inductively Defined Types, Lecture Notes in Comput. Sci. 417, 1990.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"334552_CR13","doi-asserted-by":"crossref","unstructured":"Dybjer, P.: Inductive sets and families in Martin-L\u00f6f's type theory and their set-theoretic semantics, in G. Huet and G. Plotkin (eds.), Logical Frameworks, 1991.","DOI":"10.1017\/CBO9780511569807.012"},{"key":"334552_CR14","doi-asserted-by":"crossref","unstructured":"Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory, J. Symbolic Logic\n65(2) (2000).","DOI":"10.2307\/2586554"},{"key":"334552_CR15","doi-asserted-by":"crossref","unstructured":"Goguen, H.: A typed operational semantics for type theory, Ph.D. Thesis, University of Edinburgh, 1994.","DOI":"10.1007\/BFb0014053"},{"key":"334552_CR16","unstructured":"Harper, R., Honsell, F. and Plotkin, G.: A framework for defining logics, in Proc. 2nd Ann. Symp. on Logic in Computer Science, IEEE, 1987."},{"issue":"1","key":"334552_CR17","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/0304-3975(90)90108-T","volume":"89","author":"R. Harper","year":"1991","unstructured":"Harper, R. and Pollack, R.: Type checking with universes, Theoret. Comput. Sci.\n89(1) (1991), 107\u2013136.","journal-title":"Theoret. Comput. Sci."},{"key":"334552_CR18","unstructured":"Haskell: Haskell WWWSite, http:\/\/www.haskell.org."},{"key":"334552_CR19","doi-asserted-by":"crossref","unstructured":"Huet, G.: The constructive engine, in R. Narasimhan (ed.), A Perspective in Theoretical Computer Science, Commemorative Volume for Gift Siromoney, World Scientific, 1989.","DOI":"10.1142\/9789814368452_0004"},{"key":"334552_CR20","doi-asserted-by":"crossref","unstructured":"Jones, A., Luo, Z. and Soloviev, S.: Some proof-theoretic and algorithmic aspects of coercive subtyping, in E. Gimenez and C. Paulin-Mohring (eds.), Types for Proofs and Programs, Proc. of the Inter. Conf. TYPES'96, Lecture Notes in Comput. Sci. 1512, 1998.","DOI":"10.1007\/BFb0097792"},{"key":"334552_CR21","doi-asserted-by":"crossref","unstructured":"Luo, Z.: Program specification and data refinement in type theory, in Proc. of the Fourth Inter. Joint Conf. on the Theory and Practice of Software Development (TAPSOFT), Lecture Notes in Comput. Sci. 493, 1991. Also as LFCS report ECS-LFCS\u201391\u2013131, Dept. of Computer Science, Edinburgh University.","DOI":"10.1007\/3-540-53982-4_9"},{"key":"334552_CR22","unstructured":"Luo, Z.: A unifying theory of dependent types: The schematic approach, in Proc. of Symp. on Logical Foundations of Computer Science (Logic at Tver'92), Lecture Notes in Comput. Sci. 620, Also as LFCS Report ECS-LFCS\u201392\u2013202, Dept. of Computer Science, University of Edinburgh."},{"key":"334552_CR23","doi-asserted-by":"crossref","unstructured":"Luo, Z.: Program specification and data refinement in type theory, Math. Structures Comput. Sci. 3(3) (1993).","DOI":"10.1017\/S0960129500000256"},{"key":"334552_CR24","doi-asserted-by":"crossref","unstructured":"Luo, Z.: Computation and Reasoning: A Type Theory for Computer Science, Oxford University Press, 1994.","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"issue":"1","key":"334552_CR25","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1093\/logcom\/9.1.105","volume":"9","author":"Z. Luo","year":"1991","unstructured":"Luo, Z.: Coercive subtyping, J. Logic Comput.\n9(1) (1991), 105\u2013130.","journal-title":"J. Logic Comput."},{"key":"334552_CR26","unstructured":"Luo, Z. and Callaghan, P.: Coercive subtyping and lexical semantics (extended abstract), in LACL'98, 1998."},{"key":"334552_CR27","doi-asserted-by":"crossref","unstructured":"Luo, Z. and Callaghan, P.: Mathematical vernacular and conceptual well-formedness in mathematical language, in Proceedings of the 2nd Inter. Conf. on Logical Aspects of Computational Linguistics, Lecture Notes in Comput. Sci.\/Lecture Notes in Artif. Intell. 1582, 1998.","DOI":"10.1007\/3-540-48975-4_12"},{"key":"334552_CR28","doi-asserted-by":"crossref","unstructured":"Luo, Z. and Soloviev, S.: Dependent coercions, in The 8th Inter. Conf. on Category Theory and Computer Science (CTCS'99), Edinburgh, Scotland, Electron. Notes Theor. Comput. Sci. 29, 1999.","DOI":"10.1016\/S1571-0661(05)80314-7"},{"key":"334552_CR29","doi-asserted-by":"crossref","unstructured":"Magnusson, L. and Nordstr\u00f6m, B.: The ALF proof editor and its proof engine, in Types for Proof and Programs, Lecture Notes in Comput. Sci., 1994.","DOI":"10.1007\/3-540-58085-9_78"},{"key":"334552_CR30","unstructured":"Martin-L\u00f6f, P.: Intuitionistic Type Theory, Bibliopolis, 1984."},{"key":"334552_CR31","unstructured":"McBride, C.: Dependently typed functional programs and their proofs, Ph.D. Thesis, University of Edinburgh, 2000."},{"key":"334552_CR32","unstructured":"Nordstr\u00f6m, B., Petersson, K. and Smith, J.: Programming in Martin-L\u00f6f's Type Theory: An Introduction, Oxford University Press, 1990."},{"key":"334552_CR33","doi-asserted-by":"crossref","unstructured":"Palmgren, E.: On universes in type theory, in G. Sambin and J. Smith (eds.), Twenty Five Years of Constructive Type Theory, Commemorative Volume for Gift Siromoney, Oxford University Press, 1998.","DOI":"10.1093\/oso\/9780198501275.003.0012"},{"key":"334552_CR34","unstructured":"Peyton Jones, S. L. et al.: GHC Haskell compilerWWWsite, http:\/\/www.haskell.org\/ghc."},{"key":"334552_CR35","unstructured":"Pollack, R. et al.: Lego WWWpage, http:\/\/www.dcs.ed.ac.uk\/home\/lego."},{"key":"334552_CR36","volume-title":"Outils g\u00e9n\u00e9riques de mod\u00e9lisation et de d\u00e9monstration pour la formalisation des math\u00e9matiques en th\u00e9orie des types, Application \u00e0 la th\u00e9orie des cat\u00e9gories","author":"A. Sa\u00efbi","year":"1999","unstructured":"Sa\u00efbi, A.: Outils g\u00e9n\u00e9riques de mod\u00e9lisation et de d\u00e9monstration pour la formalisation des math\u00e9matiques en th\u00e9orie des types, Application \u00e0 la th\u00e9orie des cat\u00e9gories, Ph.D. Thesis, INRIA, Rocquencourt, 1999."},{"key":"334552_CR37","doi-asserted-by":"crossref","unstructured":"Smith, J.: The independence of Peano's fourth axiom from Martin-L\u00f6f's type theory without universes, J. Symbolic Logic\n53(3) (1988).","DOI":"10.2307\/2274575"},{"key":"334552_CR38","doi-asserted-by":"crossref","unstructured":"Soloviev, S. and Luo, Z.: Coercion completion and conservativity in coercive subtyping, Ann. Pure Appl. Logic (2000).","DOI":"10.1016\/S0168-0072(01)00063-X"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1010648911114.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1010648911114\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1010648911114.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:31:18Z","timestamp":1749123078000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1010648911114"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,7]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2001,7]]}},"alternative-id":["334552"],"URL":"https:\/\/doi.org\/10.1023\/a:1010648911114","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,7]]}}}