{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:32:23Z","timestamp":1725489143294},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540002253"},{"type":"electronic","value":"9783540362067"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36206-1_3","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T07:23:08Z","timestamp":1187248988000},"page":"18-32","source":"Crossref","is-referenced-by-count":2,"title":["Encoding Generic Judgments"],"prefix":"10.1007","author":[{"given":"Dale","family":"Miller","sequence":"first","affiliation":[]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,12,16]]},"reference":[{"key":"3_CR1","unstructured":"Jawahar Chirimar. Proof Theoretic Approach to Specification Languages. PhD thesis, University of Pennsylvania, February 1995."},{"key":"3_CR2","unstructured":"Jolle Despeyroux. A higher-order specification of the \u03c0-calculus. In Proc. of the IFIP International Conference on Theoretical Computer Science, IFIP TCS\u20192000, Sendai, Japan, August 17\u201319, 2000., August 2000."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"M. P. Fiore, G. D. Plotkin, and D. Turi. Abstract syntax and variable binding. In 14th Annual Symposium on Logic in Computer Science, pages 193\u2013202. IEEE Computer Society Press, 1999.","DOI":"10.1109\/LICS.1999.782615"},{"key":"3_CR4","unstructured":"Jean-Yves Girard. A fixpoint theorem in linear logic. Email to the linear@cs.stanford.edu mailing list, February 1992."},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax involving binders. In 14th Annual Symposium on Logic in Computer Science, pages 214\u2013224. IEEE Computer Society Press, 1999.","DOI":"10.1109\/LICS.1999.782617"},{"issue":"2","key":"3_CR6","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/S0304-3975(00)00095-5","volume":"253","author":"F. Honsell","year":"2001","unstructured":"Furio Honsell, Marino Miculan, and Ivan Scagnetto. Pi-calculus in (co)inductive type theory. TCS, 253(2):239\u2013285, 2001.","journal-title":"TCS"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"M. Hofmann. Semantical analysis of higher-order abstract syntax. In 14th Annual Symposium on Logic in Computer Science, pages 204\u2013213. IEEE Computer Society Press, 1999.","DOI":"10.1109\/LICS.1999.782616"},{"issue":"5","key":"3_CR8","doi-asserted-by":"publisher","first-page":"635","DOI":"10.1093\/logcom\/1.5.635","volume":"1","author":"L. Halln\u00e4s","year":"1991","unstructured":"Lars Halln\u00e4s and Peter Schroeder-Heister. A proof-theoretic approach to logic programming. ii. Programs as definitions. Journal of Logic and Computation, 1(5):635\u2013660, October 1991.","journal-title":"Journal of Logic and Computation"},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G\u00e9rard Huet. A unification algorithm for typed \u03bb-calculus. TCS, 1:27\u201357, 1975.","journal-title":"TCS"},{"key":"3_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/BFb0039592","volume-title":"Natural semantics","author":"G. Kahn","year":"1987","unstructured":"Gilles Kahn. Natural semantics. In Proc. of the Symposium on Theoretical Aspects of Computer Science, volume 247 of LNCS, pages 22\u201339. March 1987."},{"key":"3_CR11","unstructured":"Raymond McDowell. Reasoning in a Logic with Definitions and Induction. PhD thesis, University of Pennsylvania, December 1997."},{"key":"3_CR12","unstructured":"Dale Miller. Abstractions in logic programming. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 329\u2013359. Academic Press, 1990."},{"issue":"4","key":"3_CR13","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":"3_CR14","unstructured":"Dale Miller. Unification of simply typed lambda-terms as logic programming. In Eighth International Logic Programming Conference, pages 255\u2013269, Paris, France, June 1991. MIT Press."},{"issue":"1","key":"3_CR15","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0304-3975(96)00045-X","volume":"165","author":"D. Miller","year":"1996","unstructured":"Dale Miller. Forum: A multiple-conclusion specification language. TCS, 165(1):201\u2013232, September 1996.","journal-title":"TCS"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Dale Miller. Abstract syntax for variable binders: An overview. In John Lloyd and et. al., editors, Computational Logic-CL 2000, number 1861 in LNAI, pages 239\u2013253. Springer, 2000.","DOI":"10.1007\/3-540-44957-4_16"},{"key":"3_CR17","unstructured":"Dale Miller. Encoding generic judgments: Preliminary results. In R.L. Crole S.J. Ambler and A. Momigliano, editors, ENTCS, volume 58. Elsevier, 2001. Proceedings of the MERLIN 2001 Workshop, Siena."},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Raymond McDowell and Dale Miller. A logic for reasoning with higher-order abstract syntax. In Glynn Winskel, editor, Proceedings, Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 434\u2013445, Warsaw, Poland, July 1997. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1997.614968"},{"key":"3_CR19","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0304-3975(99)00171-1","volume":"232","author":"R. McDowell","year":"2000","unstructured":"Raymond McDowell and Dale Miller. Cut-elimination for a logic with definitions and induction. TCS, 232:91\u2013119, 2000.","journal-title":"TCS"},{"issue":"1","key":"3_CR20","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/504077.504080","volume":"3","author":"R. McDowell","year":"2002","unstructured":"Raymond McDowell and Dale Miller. Reasoning with higher-order abstract syntax in a logical framework. ACM Transactions on Computational Logic, 3(1):80\u2013136, January 2002.","journal-title":"ACM Transactions on Computational Logic"},{"key":"3_CR21","unstructured":"Raymond McDowell, Dale Miller, and Catuscia Palamidessi. Encoding transition systems in sequent calculus. TCS, 197(1\u20132), 2001. To appear."},{"key":"3_CR22","unstructured":"Dale Miller and Gopalan Nadathur. A computational logic approach to syntax and semantics. Presented at the Tenth Symposium of the Mathematical Foundations of Computer Science, IBM Japan, May 1985."},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Dale Miller and Gopalan Nadathur. Some uses of higher-order logic in computational linguistics. In Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics, pages 247\u2013255. Association for Computational Linguistics, Morristown, New Jersey, 1986.","DOI":"10.3115\/981131.981165"},{"key":"3_CR24","unstructured":"Dale Miller and Gopalan Nadathur. A logic programming approach to manipulating formulas and programs. In Seif Haridi, editor, IEEE Symposium on Logic Programming, pages 379\u2013388, San Francisco, September 1987."},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Dale Miller and Catuscia Palamidessi. Foundational aspects of syntax. In Pierpaolo Degano, Roberto Gorrieri, Alberto Marchetti-Spaccamela, and Peter Wegner, editors, ACM Computing Surveys Symposium on Theoretical Computer Science: A Perspective, volume 31. ACM, Sep 1999.","DOI":"10.1145\/333580.333590"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, Part II. Information and Computation, pages 41\u201377, 1992.","DOI":"10.1016\/0890-5401(92)90009-5"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow. Higher-order critical pairs. In G. Kahn, editor, LICS91, pages 342\u2013349. IEEE, July 1991.","DOI":"10.1109\/LICS.1991.151658"},{"key":"3_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/3-540-48660-7_25","volume-title":"CADE16","author":"G. Nadathur","year":"1999","unstructured":"Gopalan Nadathur and Dustin J. Mitchell. System description: Teyjus\u2014a compiler and abstract machine based implementation of Lambda Prolog. In H. Ganzinger, ed., CADE16, pages 287\u2013291, Trento, Italy, July 1999. LNCS."},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363\u2013397, September 1989.","DOI":"10.1007\/BF00248324"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pages 199\u2013208. ACM Press, June 1988.","DOI":"10.1145\/53990.54010"},{"key":"3_CR31","volume-title":"A structural approach to operational semantics","author":"G. Plotkin","year":"1981","unstructured":"G. Plotkin. A structural approach to operational semantics. DAIMI FN-19, Aarhus University, Aarhus, Denmark, September 1981."},{"key":"3_CR32","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of FOSSACS\u201901","author":"C. R\u00f6ckl","year":"2001","unstructured":"C. R\u00f6ckl, D. Hirschko., and S. Berghofer. Higher-order abstract syntax with induction in Isabelle\/HOL: Formalizing the pi-calculus and mechanizing the theory of contexts. In Proceedings of FOSSACS\u201901, LNCS, 2001."},{"issue":"2","key":"3_CR33","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0304-3975(96)00075-8","volume":"167","author":"D. Sangiorgi","year":"1996","unstructured":"Davide Sangiorgi. \u03c0-calculus, internal mobility and agent-passing calculi. TCS, 167(2):235\u2013274, 1996.","journal-title":"TCS"},{"key":"3_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/BFb0031929","volume-title":"Nonclassical Logics and Information Processing","author":"P. Schroeder-Heister","year":"1992","unstructured":"Peter Schroeder-Heister. Cut-elimination in logics with definitional reflection. In D. Pearce and H. Wansing, editors, Nonclassical Logics and Information Processing, volume 619 of LNCS, pages 146\u2013171. Springer, 1992."},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Peter Schroeder-Heister. Rules of definitional reflection. In M. Vardi, editor, Eighth Annual Symposium on Logic in Computer Science, pages 222\u2013232. IEEE Computer Society Press, IEEE, June 1993.","DOI":"10.1109\/LICS.1993.287585"},{"key":"3_CR36","unstructured":"Alwen F. Tiu. An extension of L-lambda unification. Draft, available via http:\/\/www.cse.psu.edu\/~tiu\/llambdaext.pdf , September 2002."},{"key":"3_CR37","unstructured":"J\u00e9r\u00e9mie D. Wajs. Reasoning about Logic Programs Using Definitions and Induction. PhD thesis, Pennsylvania State University, 2002."}],"container-title":["Lecture Notes in Computer Science","FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36206-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T04:07:53Z","timestamp":1556770073000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36206-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540002253","9783540362067"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/3-540-36206-1_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}