{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:08:55Z","timestamp":1760202535319},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540140313"},{"type":"electronic","value":"9783540391852"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-39185-1_10","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T16:13:43Z","timestamp":1193415223000},"page":"162-181","source":"Crossref","is-referenced-by-count":6,"title":["Holes with Binding Power"],"prefix":"10.1007","author":[{"given":"Georgi I.","family":"Jojgov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,4,15]]},"reference":[{"key":"10_CR1","unstructured":"Henk Barendregt. Lambda calculi with types. In Abramsky et al., editor, Handbook of Logic in Computer Science, pages 117\u2013309. Oxford University Press, 1992."},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"R. Bloo, Fairouz Kamareddine, Twan Laan, and Rob Nederpelt. Parameters in Pure Type Systems. In Proceedings of LATIN\u201902. Springer, 2002.","DOI":"10.1007\/3-540-45995-2_34"},{"key":"10_CR3","unstructured":"Mirna Bognar. Contexts in Lambda Calculus. PhD thesis, VU Amsterdam, 2002."},{"key":"10_CR4","unstructured":"N.G. de Bruijn. A Survey of the Project AUTOMATH. In Hindley and Seldin, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980."},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Herman Geuvers and G.I. Jojgov. Open proofs and open terms: a basis for interactive logic. In Bradfield, editor, Proceedings of CSL\u201902. Springer, 2002.","DOI":"10.1007\/3-540-45793-3_36"},{"key":"10_CR6","unstructured":"J.H. Geuvers. Logics and Type systems. PhD thesis, University of Nijmegen."},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Zhaohui Luo. PAL+: A lambda-free logical framework. Journal of Functional Programming, to appear.","DOI":"10.1017\/S0956796802004525"},{"key":"10_CR8","unstructured":"Lena Magnusson. The Implementation of ALF \u2014 a Proof Editor based on Martin-L\u00f6f Monomorphic Type Theory with Explicit Substitutions. PhD thesis, Chalmers University of Technology \/ G\u00f6teborg University, 1995."},{"key":"10_CR9","unstructured":"Conor McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, 1999."},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Dale Miller. Unification under a mixed prefix. J. of Symbolic Computation, 1992.","DOI":"10.1016\/0747-7171(92)90011-R"},{"issue":"3","key":"10_CR11","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L. C. Paulson","year":"1989","unstructured":"Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5(3):363\u2013397, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of LFCS\u201994, St. Petersburg, Russia","author":"P. Severi","year":"1994","unstructured":"P. Severi and E. Poll. Pure Type Systems with definitions. In Proc. of LFCS\u201994, St. Petersburg, Russia, number 813 in LNCS, Berlin, 1994. Springer Verlag."},{"key":"10_CR13","unstructured":"M. Strecker. Construction and Deduction in Type Theories. PhD thesis, Universit\u00e4t Ulm, 1999."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-39185-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T21:48:45Z","timestamp":1556920125000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-39185-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540140313","9783540391852"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-39185-1_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}