{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T10:16:26Z","timestamp":1648894586120},"reference-count":23,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2000,2,1]],"date-time":"2000-02-01T00:00:00Z","timestamp":949363200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4915,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2000,2]]},"DOI":"10.1016\/s0304-3975(99)00175-9","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T15:42:52Z","timestamp":1027611772000},"page":"187-229","source":"Crossref","is-referenced-by-count":3,"title":["The calculus of constructions as a framework for proof search with set variable instantiation"],"prefix":"10.1016","volume":"232","author":[{"given":"Amy","family":"Felty","sequence":"first","affiliation":[]}],"member":"78","reference":[{"issue":"3","key":"10.1016\/S0304-3975(99)00175-9_BIB1","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/BF00881874","article-title":"Z-match: an inference rule for incrementally elaborating set instantiation","volume":"11","author":"Bailin","year":"1993","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"10.1016\/S0304-3975(99)00175-9_BIB2","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1017\/S0956796800020025","article-title":"Introduction to generalized type systems","volume":"1","author":"Barendregt","year":"1991","journal-title":"J. Functional Programming"},{"key":"10.1016\/S0304-3975(99)00175-9_BIB3","first-page":"53","article-title":"A maximal method for set variables in automatic theorem proving","volume":"9","author":"Bledsoe","year":"1979","journal-title":"Machine Intelligence"},{"issue":"3","key":"10.1016\/S0304-3975(99)00175-9_BIB4","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/BF00881869","article-title":"SET-VAR","volume":"11","author":"Bledsoe","year":"1993","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/S0304-3975(99)00175-9_BIB5","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(99)00175-9_BIB6","unstructured":"R.L. Constable et al., Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, Englewood Cliff, NJ, 1986."},{"issue":"2\/3","key":"10.1016\/S0304-3975(99)00175-9_BIB7","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(99)00175-9_BIB8","unstructured":"C. Cornes, J. Courant, J.-C. Filli\u00e2tre, G. Huet, P. Manoury, C. Paulin-Mohring, C. Mu\u00f1oz, C. Murthy, C. Parent, A. Sa\u0131\u0308bi, B. Werner, The Coq Proof Assistant reference manual, Tech. Report, INRIA, 1995."},{"key":"10.1016\/S0304-3975(99)00175-9_BIB9","unstructured":"G. Dowek, D\u00e9monstration Automatique dans le Calcul des Constructions, Ph.D. Thesis, Universit\u00e9 Paris VII, December 1991."},{"issue":"3","key":"10.1016\/S0304-3975(99)00175-9_BIB10","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1093\/logcom\/3.3.287","article-title":"A complete proof synthesis method for the cube of type systems","volume":"3","author":"Dowek","year":"1993","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0304-3975(99)00175-9_BIB11","doi-asserted-by":"crossref","unstructured":"G. Dowek, T. Hardin, C. Kirchner, Higher-order unification via explicit substitutions, in: 10th Ann. Symp. on Logic in Computer Science, 1995, pp. 366\u2013374.","DOI":"10.1109\/LICS.1995.523271"},{"key":"10.1016\/S0304-3975(99)00175-9_BIB12","doi-asserted-by":"crossref","unstructured":"A. Felty, Encoding the calculus of constructions in a higher-order logic, in: 8th Ann. Symp. on Logic in Computer Science, June 1993, pp. 233\u2013244.","DOI":"10.1109\/LICS.1993.287584"},{"issue":"1","key":"10.1016\/S0304-3975(99)00175-9_BIB13","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/BF00881900","article-title":"Implementing tactics and tacticals in a higher-order logic programming language","volume":"11","author":"Felty","year":"1993","journal-title":"J. Automated Reasoning"},{"key":"10.1016\/S0304-3975(99)00175-9_BIB14","doi-asserted-by":"crossref","unstructured":"A. Felty, Proof search with set variable instantiation in the calculus of constructions, in: 13th Internat. Conf. on Automated Deduction, Springer, Berlin, Lecture Notes in Computer Science, 1996, pp. 658\u2013672.","DOI":"10.1007\/3-540-61511-3_120"},{"key":"10.1016\/S0304-3975(99)00175-9_BIB15","unstructured":"M.J.C. Gordon, T.F. Melham, Introduction to HOL \u2013 A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, Cambridge, 1993."},{"issue":"1","key":"10.1016\/S0304-3975(99)00175-9_BIB16","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A framework for defining logics","volume":"40","author":"Harper","year":"1993","journal-title":"J. ACM"},{"key":"10.1016\/S0304-3975(99)00175-9_BIB17","unstructured":"W.A. Howard, The formulae-as-type notion of construction, 1969, in: To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, Academic Press, 1980, New York, pp. 479\u2013490."},{"key":"10.1016\/S0304-3975(99)00175-9_BIB18","unstructured":"G. Huet (Ed.), A uniform approach to type theory, Logical Foundations of Functional Programming, Addison Wesley, Reading, MA, 1990."},{"key":"10.1016\/S0304-3975(99)00175-9_BIB19","unstructured":"L. Magnusson, The implementation of ALF: a proof editor based on Martin-L\u00f6f's monomorphic type theory with explicit substitution, Ph.D. Thesis, Chalmers University of Technology\/G\u00f6teborg University, January, 1995."},{"key":"10.1016\/S0304-3975(99)00175-9_BIB20","unstructured":"P. Martin-L\u00f6f, Intuitionistic Type Theory, Studies in Proof Theory Lecture Notes, BIBLIOPOLIS, Napoli, 1984."},{"key":"10.1016\/S0304-3975(99)00175-9_BIB21","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","article-title":"Uniform proofs as a foundation for logic programming","volume":"51","author":"Miller","year":"1991","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(99)00175-9_BIB22","unstructured":"C. Mu\u00f1oz, A calculus of substitutions for incomplete-proof representation in type theory, Ph.D. Thesis, Universit\u00e9 Paris 7, INRIA Research Report RR-3309 (English version), 1997."},{"key":"10.1016\/S0304-3975(99)00175-9_BIB23","doi-asserted-by":"crossref","unstructured":"L.C. Paulson, Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, vol. 828, Springer, Berlin, 1994.","DOI":"10.1007\/BFb0030541"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397599001759?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397599001759?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,10]],"date-time":"2020-01-10T16:55:57Z","timestamp":1578675357000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397599001759"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,2]]},"references-count":23,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2000,2]]}},"alternative-id":["S0304397599001759"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(99)00175-9","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2000,2]]}}}