{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T19:13:10Z","timestamp":1649013190091},"reference-count":18,"publisher":"Elsevier BV","issue":"7","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3619,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1016\/s1571-0661(04)80757-6","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"50-68","source":"Crossref","is-referenced-by-count":0,"title":["Tactics and Parameters"],"prefix":"10.1016","volume":"85","author":[{"given":"Gueorgui","family":"Jojgov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB1","series-title":"Handbook of Logic in Computer Science","first-page":"117","article-title":"Lambda calculi with types","author":"Henk","year":"1992"},{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB2","unstructured":"S. Berardi. Towards a methematical analysis of the Coquand-Huet calculus and the other systems in Barendregt's cube. Technical report, Carnegie-Mellon University and Universita di Torino, 1989."},{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB3","doi-asserted-by":"crossref","unstructured":"R. Bloo, Fairouz Kamareddine, Twan Laan, and Rob Nederpelt. Parameters in Pure Type Systems. In Proceedings of LATIN'02. Springer, 2002.","DOI":"10.1007\/3-540-45995-2_34"},{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB4","unstructured":"Mirna Bognar. Contexts in Lambda Calculus. PhD thesis, Vrije Universiteit Amsterdam, 2002."},{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB5","series-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","article-title":"A Survey of the Project AUTOMATH","author":"de Bruijn","year":"1980"},{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB6","unstructured":"Herman Geuvers. Logics and Type systems. PhD thesis, University of Nijmegen, 1993."},{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB7","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'02. Springer, 2002.","DOI":"10.1007\/3-540-45793-3_36"},{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB8","doi-asserted-by":"crossref","unstructured":"Gueorgui Jojgov. Holes with Binding Power. In Proceedings of TYPES'02. Springer, 2003.","DOI":"10.1007\/3-540-39185-1_10"},{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB9","unstructured":"Zhaohui Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, July 1990."},{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB10","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.1016\/S1571-0661(04)80757-6_NEWBIB11","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":"10.1016\/S1571-0661(04)80757-6_NEWBIB12","unstructured":"Conor McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, 1999."},{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB13","doi-asserted-by":"crossref","DOI":"10.1016\/0747-7171(92)90011-R","article-title":"Unification under a mixed prefix","author":"Miller","year":"1992","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB14","unstructured":"C\u00e9sar A. Mu\u00f1oz. A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory. PhD thesis, INRIA, November 1997."},{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB15","doi-asserted-by":"crossref","unstructured":"P. Severi and E. Poll. Pure Type Systems with definitions. In Proc. of LFCS'94, St. Petersburg, Russia, number 813 in LNCS, Berlin, 1994. Springer Verlag.","DOI":"10.1007\/3-540-58140-5_30"},{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB16","unstructured":"M. Strecker. Construction and Deduction in Type Theories. PhD thesis, Universit\u00e4t Ulm, 1999."},{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB17","doi-asserted-by":"crossref","DOI":"10.1006\/inco.1995.1057","article-title":"Parallel reductions in \u03bb-calculus","volume":"118","author":"Takahashi","year":"1995","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)80757-6_NEWBIB18","unstructured":"J. Terlouw. Een nadere bewijstheoretische analyse van GSTTs. Technical report, University of Nijmegen, 1989."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104807576?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104807576?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T07:14:16Z","timestamp":1585898056000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104807576"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":18,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S1571066104807576"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80757-6","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}