{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T23:40:27Z","timestamp":1737502827984,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540422549"},{"type":"electronic","value":"9783540457442"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45744-5_31","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T21:02:07Z","timestamp":1193432527000},"page":"386-400","source":"Crossref","is-referenced-by-count":1,"title":["More On Implicit Syntax"],"prefix":"10.1007","author":[{"given":"Marko","family":"Luther","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,8]]},"reference":[{"key":"31_CR1","series-title":"Technical report","volume-title":"The Coq proof assistant reference manual-Version 6.3.1","author":"B. Barras","year":"1999","unstructured":"B. Barras et al. The Coq proof assistant reference manual-Version 6.3.1. Technical report, INRIA, France, 1999."},{"key":"31_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/3-540-44659-1_3","volume-title":"Proc. of TPHOLs\u201900","author":"S. Berghofer","year":"2000","unstructured":"S. Berghofer, T. Nipkow. Proof terms for simply typed higher order logic. In Proc. of TPHOLs\u201900, volume 1869 of LNCS, pp. 38\u201353. Springer, 2000."},{"issue":"2\/3","key":"31_CR3","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"Th. Coquand","year":"1988","unstructured":"Th. Coquand, G. Huet. The Calculus of Constructions. Information and Computation, 76(2\/3):95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"H. Geuvers. The Church-Rosser property for \u03b2\u03b7-reduction in typed \u03bb-calculi. In Proc. of LICS\u201992, pp. 453\u2013460. IEEE Press, 1992.","DOI":"10.1109\/LICS.1992.185556"},{"key":"31_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/BFb0055133","volume-title":"Proc. of TPHOLs\u201998","author":"W. O. D. Griffoen","year":"1998","unstructured":"W. O. D. Griffoen, M. Huisman. A comparison of PVS and Isabelle\/HOL. In Proc. of TPHOLs\u201998, volume 1479 of LNCS, pp. 123\u2013142. Springer, 1998."},{"key":"31_CR6","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W. Goldfarb","year":"1981","unstructured":"W. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225\u2013230, 1981.","journal-title":"Theoretical Computer Science"},{"key":"31_CR7","series-title":"Technical Report TR-95-1","volume-title":"On implicit arguments","author":"M. Hagiya","year":"1995","unstructured":"M. Hagiya, Y. Toda. On implicit arguments. Technical Report TR-95-1, Department of Information Science, University of Tokyo, 1995."},{"key":"31_CR8","volume-title":"A Perspective in Theoretical Computer Science","author":"G. Huet","year":"1989","unstructured":"G. Huet. The Constructive Engine. In A Perspective in Theoretical Computer Science. World Scientific Publishing, Singapore, 1989."},{"key":"31_CR9","unstructured":"Z. Luo, R. Pollack. LEGO Proof Development System. University of Edinburgh, 1992. Technical Report ECS-LFCS-92-211."},{"issue":"4","key":"31_CR10","doi-asserted-by":"publisher","first-page":"707","DOI":"10.1145\/291891.291892","volume":"20","author":"O. Lee","year":"1998","unstructured":"O. Lee, K. Yi. Proofs about a folklore let-polymorphic type inference algorithm. ACM TOPLAS, 20(4):707\u2013723, 1998.","journal-title":"ACM TOPLAS"},{"issue":"4","key":"31_CR11","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. J. Logic Comput., 1(4):497\u2013536, 1991.","journal-title":"J. Logic Comput."},{"key":"31_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the Conf. TLCA\u201901, Krakow, Poland, May 2-5, 2001","author":"A. Miquel","year":"2001","unstructured":"A. Miquel. The implicit calculus of constructions. In Proc. of the Conf. TLCA\u201901, Krakow, Poland, May 2-5, 2001, LNCS. Springer, Berlin, 2001."},{"key":"31_CR13","doi-asserted-by":"crossref","unstructured":"C. Mu\u00f1oz. Proof-term synthesis on dependent-type systems via explicit substitutions. Theoretical Computer Science, 2001. To appear.","DOI":"10.1016\/S0304-3975(00)00196-1"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"G. Necula, P. Lee. Efficient representation and validation of proofs. In Proc. of LICS\u201998, pp. 93\u2013104. IEEE Press, 1998.","DOI":"10.1109\/LICS.1998.705646"},{"key":"31_CR15","unstructured":"R. Pollack. Implicit syntax. In G. Huet, G. Plotkin, eds., Informal Proc. Of the 1st Workshop on Logical Frameworks (LF\u201990), Antibes. 1990."},{"key":"31_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-48167-2_13","volume-title":"Proc. of TYPES\u201998","author":"F. Pfenning","year":"1999","unstructured":"F. Pfenning, C. Sch\u00fcrmann. Algorithms for equality and unification in the presence of notational definitions. In T. Altenkirch, W. Naraschewski, B. Reus, eds., Proc. of TYPES\u201998, volume 1657 of LNCS, pp. 179\u2013193. Springer, 1999."},{"key":"31_CR17","doi-asserted-by":"crossref","unstructured":"B. Pierce, D. Turner. Local type inference. In Conf. Record of POPL\u201998, pp. 252\u2013265. ACM Press, 1998.","DOI":"10.1145\/268946.268967"},{"key":"31_CR18","doi-asserted-by":"crossref","unstructured":"M. Strecker, M. Luther, F. von Henke. Interactive and automated proof construction in type theory. In W. Bibel, P. Schmitt, eds., Automated Deduction \u2014 A Basis for Applications, volume I, chapter 3. Kluwer, 1998.","DOI":"10.1007\/978-94-017-0435-9_3"},{"key":"31_CR19","series-title":"Ph. D. thesis","volume-title":"Construction and Deduction in Type Theories","author":"M. Strecker","year":"1999","unstructured":"M. Strecker. Construction and Deduction in Type Theories. Ph. D. thesis, Fakult\u00f4t f\u00fcr Informatik, Universit\u00f4t Ulm, 1999. http:\/\/www.informatik.uni-ulm.de\/ki\/Strecker\/phd.html"},{"key":"31_CR20","series-title":"Lect Notes Comput Sci","first-page":"851","volume-title":"Proc. of the 7th Intl. Conf. TAPSOFT\u201997","author":"F. Henke von","year":"1997","unstructured":"F. von Henke, M. Luther, M. Strecker. Typelab: An environment for modular program development. In M. Bidoit, M. Dauchet, eds., Proc. of the 7th Intl. Conf. TAPSOFT\u201997, volume 1214 of LNCS, pp. 851\u2013854. Springer, 1997."},{"issue":"1-3","key":"31_CR21","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/S0168-0072(98)00047-5","volume":"98","author":"J. B. Wells","year":"1999","unstructured":"J. B. Wells. Typability and type checking in System F are equivalent and undecidable. Ann. Pure \u2130 Appl. Logics, 98(1-3):111\u2013156, 1999.","journal-title":"Ann. Pure \u2130 Appl. Logics"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45744-5_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T23:09:59Z","timestamp":1737500999000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45744-5_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422549","9783540457442"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-45744-5_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]}}}