{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T16:01:16Z","timestamp":1765123276292},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540442400"},{"type":"electronic","value":"9783540457930"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45793-3_36","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T08:03:26Z","timestamp":1187251406000},"page":"537-552","source":"Crossref","is-referenced-by-count":19,"title":["Open Proofs and Open Terms: A Basis for Interactive Logic"],"prefix":"10.1007","author":[{"given":"Herman","family":"Geuvers","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gueorgui I.","family":"Jojgov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,2]]},"reference":[{"key":"36_CR1","unstructured":"H. Barendregt and H. Geuvers. Proof assistants using dependent type systems. In Handbook of Automated Reasoning. Elsevier Science Publishers B. V., 1999."},{"key":"36_CR2","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":"36_CR3","unstructured":"H. P. Barendregt. The \u03bb-calculus: Its syntax and semantics. North-Holland, 1984."},{"key":"36_CR4","unstructured":"Mirna Bognar. PhD thesis, VU Amsterdam, to appear, 2002."},{"key":"36_CR5","unstructured":"J. H. Geuvers. Logics and Type systems. PhD thesis, University of Nijmegen."},{"key":"36_CR6","unstructured":"G. I. Jojgov. Systems for open terms: An overview. Technical Report CSR 01-03, Technische Universiteit Eindhoven, 2001."},{"key":"36_CR7","unstructured":"Zhaohui Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, July 1990."},{"key":"36_CR8","doi-asserted-by":"crossref","unstructured":"Zhaohui Luo. PAL+: A lambda-free logical framework. Lournal of Functional Programming, to appear.","DOI":"10.1017\/S0956796802004525"},{"key":"36_CR9","unstructured":"Lena Magnusson. The Implementation of ALF-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":"36_CR10","unstructured":"Conor McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, 1999."},{"issue":"4","key":"36_CR11","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497\u2013536, 1991.","journal-title":"Journal of Logic and Computation"},{"key":"36_CR12","unstructured":"C\u00e9sar A. Mu\u00f1oz. A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory. PhD thesis, INRIA, November 1997."},{"issue":"3","key":"36_CR13","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":"36_CR14","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Logical frameworks. In Handbook of Automated Reasoning, pages 1063\u20131147. 2001.","DOI":"10.1016\/B978-044450813-3\/50019-9"},{"key":"36_CR15","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":"36_CR16","unstructured":"M. Strecker. Construction and Deduction in Type Theories. PhD thesis, Universit\u00e4t Ulm, 1998."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45793-3_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T19:00:10Z","timestamp":1550775610000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45793-3_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540442400","9783540457930"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45793-3_36","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}