{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:11Z","timestamp":1761611171876,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2005,10,1]],"date-time":"2005-10-01T00:00:00Z","timestamp":1128124800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2005,10]]},"abstract":"<jats:p>\n            The operational semantics of a computation system is often presented as inference rules or, equivalently, as logical theories. Specifications can be made more declarative and high level if syntactic details concerning bound variables and substitutions are encoded directly into the logic using term-level abstractions (\u03bb-abstraction) and proof-level abstractions (eigenvariables). When one wishes to use such logical theories to support reasoning about properties of computation, the usual quantifiers and proof-level abstractions do not seem adequate: proof-level abstraction of variables with scope over sequents (\n            <jats:italic>global<\/jats:italic>\n            scope) as well as over only formulas (\n            <jats:italic>local<\/jats:italic>\n            scope) seem required for many examples. We will present a sequent calculus that provides this local notion of proof-level abstraction via\n            <jats:italic>generic judgment<\/jats:italic>\n            and a new quantifier, \u2207, which explicitly manipulates such local scope. Intuitionistic logic extended with \u2207 satisfies cut-elimination even when the logic is additionally strengthened with a proof theoretic notion of definitions. The resulting logic can be used to encode naturally a number of examples involving abstractions, and we illustrate the uses of \u2207 with the \u03c0-calculus and an encoding of provability of an object-logic.\n          <\/jats:p>","DOI":"10.1145\/1094622.1094628","type":"journal-article","created":{"date-parts":[[2005,11,7]],"date-time":"2005-11-07T16:00:45Z","timestamp":1131379245000},"page":"749-783","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":90,"title":["A proof theory for generic judgments"],"prefix":"10.1145","volume":"6","author":[{"given":"Dale","family":"Miller","sequence":"first","affiliation":[{"name":"INRIA-Futurs &amp; \u00c9cole polytechnique"}]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[{"name":"\u00c9cole polytechnique &amp; Penn State University"}]}],"member":"320","published-online":{"date-parts":[[2005,10]]},"reference":[{"volume-title":"Proceedings of the 12th IEEE Computer Security Foundations Workshop---CSFW'99","author":"Cervesato I.","key":"e_1_2_1_1_1","unstructured":"Cervesato , I. , Durgin , N. A. , Lincoln , P. D. , Mitchell , J. C. , and Scedrov , A . 1999. A meta-notation for protocol analysis . In Proceedings of the 12th IEEE Computer Security Foundations Workshop---CSFW'99 ( Mordano, Italy), R. Gorrieri, Ed. IEEE Computer Society Press, Los Alamitos, CA, 55--69.]] Cervesato, I., Durgin, N. A., Lincoln, P. D., Mitchell, J. C., and Scedrov, A. 1999. A meta-notation for protocol analysis. In Proceedings of the 12th IEEE Computer Security Foundations Workshop---CSFW'99 (Mordano, Italy), R. Gorrieri, Ed. IEEE Computer Society Press, Los Alamitos, CA, 55--69.]]"},{"volume-title":"Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science","author":"Cervesato I.","key":"e_1_2_1_2_1","unstructured":"Cervesato , I. and Pfenning , F . 1996. A linear logic framework . In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science ( New Brunswick, NJ). IEEE Computer Society Press, Los Alamitos, CA, 264--275.]] Cervesato, I. and Pfenning, F. 1996. A linear logic framework. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (New Brunswick, NJ). IEEE Computer Society Press, Los Alamitos, CA, 264--275.]]"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 2nd International Workshop on Extensions to Logic Programming, L.-H. Eriksson, L. Halln\u00e4s, and P. Schroeder-Heister, Eds. Lecture Notes in Artificial Intelligence","volume":"596","author":"Eriksson L.-H.","year":"1991","unstructured":"Eriksson , L.-H. 1991 . A finitary version of the calculus of partial inductive definitions . In Proceedings of the 2nd International Workshop on Extensions to Logic Programming, L.-H. Eriksson, L. Halln\u00e4s, and P. Schroeder-Heister, Eds. Lecture Notes in Artificial Intelligence , vol. 596 . Springer-Verlag, New York, 89--134.]] Eriksson, L.-H. 1991. A finitary version of the calculus of partial inductive definitions. In Proceedings of the 2nd International Workshop on Extensions to Logic Programming, L.-H. Eriksson, L. Halln\u00e4s, and P. Schroeder-Heister, Eds. Lecture Notes in Artificial Intelligence, vol. 596. Springer-Verlag, New York, 89--134.]]"},{"volume-title":"Proceedings of the 9th International Conference on Automated Deduction","author":"Felty A.","key":"e_1_2_1_6_1","unstructured":"Felty , A. and Miller , D . 1988. Specifying theorem provers in a higher-order logic programming language . In Proceedings of the 9th International Conference on Automated Deduction ( Argonne, IL). Springer-Verlag, New York, 61--80.]] Felty, A. and Miller, D. 1988. Specifying theorem provers in a higher-order logic programming language. In Proceedings of the 9th International Conference on Automated Deduction (Argonne, IL). Springer-Verlag, New York, 61--80.]]"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319608"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"volume-title":"The Collected Papers of Gerhard Gentzen","author":"Gentzen G.","key":"e_1_2_1_9_1","unstructured":"Gentzen , G. 1969. Investigations into logical deductions . In The Collected Papers of Gerhard Gentzen , M. E. Szabo, Ed. North-Holland Publishing Co., Amsterdam, The Netherlands , 68-- 131.]] Gentzen, G. 1969. Investigations into logical deductions. In The Collected Papers of Gerhard Gentzen, M. E. Szabo, Ed. North-Holland Publishing Co., Amsterdam, The Netherlands, 68-- 131.]]"},{"key":"e_1_2_1_10_1","unstructured":"Girard J.-Y. 1992. A fixpoint theorem in linear logic. Email to the linear@cs.stanford.edu mailing list.]]  Girard J.-Y. 1992. A fixpoint theorem in linear logic. Email to the linear@cs.stanford.edu mailing list.]]"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.5.635"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00171-1"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/504077.504080"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00168-2"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 6th International Logic Programming Conference","author":"Miller D.","year":"1989","unstructured":"Miller , D. 1989 . Lexical scoping as universal quantification . In Proceedings of the 6th International Logic Programming Conference ( Lisbon, Portugal). MIT Press, Cambridge, MA, 268--283.]] Miller, D. 1989. Lexical scoping as universal quantification. In Proceedings of the 6th International Logic Programming Conference (Lisbon, Portugal). MIT Press, Cambridge, MA, 268--283.]]"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.4.497"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0747-7171(92)90011-R"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 1992 Workshop on Extensions to Logic Programming","volume":"660","author":"Miller D.","year":"1993","unstructured":"Miller , D. 1993 . The &pi;-calculus as a theory in linear logic: Preliminary results . In Proceedings of the 1992 Workshop on Extensions to Logic Programming ( Bologna, Italy). E. Lamma and P. Mello, Eds. Lecture Notes in Computer Science , vol. 660 , Springer-Verlag, New York, 242--265.]] Miller, D. 1993. The &pi;-calculus as a theory in linear logic: Preliminary results. In Proceedings of the 1992 Workshop on Extensions to Logic Programming (Bologna, Italy). E. Lamma and P. Mello, Eds. Lecture Notes in Computer Science, vol. 660, Springer-Verlag, New York, 242--265.]]"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00045-X"},{"key":"e_1_2_1_22_1","volume-title":"Computational Logic (CL","author":"Miller D.","year":"2000","unstructured":"Miller , D. 2000. Abstract syntax for variable binders: An overview . In Computational Logic (CL 2000 ), J. Lloyd et. al., Eds. Lecture Notes in Artificial Intelligence, vol. 1861 . Springer-Verlag , New York, 239--253.]] Miller, D. 2000. Abstract syntax for variable binders: An overview. In Computational Logic (CL 2000), J. Lloyd et. al., Eds. Lecture Notes in Artificial Intelligence, vol. 1861. Springer-Verlag, New York, 239--253.]]"},{"key":"e_1_2_1_23_1","volume-title":"ACM Computing Surveys Symposium on Theoretical Computer Science: A Perspective, P. Degano, R. Gorrieri, A. Marchetti-Spaccamela, and P. Wegner, Eds.","volume":"31","author":"Miller D.","unstructured":"Miller , D. and Palamidessi , C . 1999. Foundational aspects of syntax . In ACM Computing Surveys Symposium on Theoretical Computer Science: A Perspective, P. Degano, R. Gorrieri, A. Marchetti-Spaccamela, and P. Wegner, Eds. Vol. 31 . ACM, New York.]] Miller, D. and Palamidessi, C. 1999. Foundational aspects of syntax. In ACM Computing Surveys Symposium on Theoretical Computer Science: A Perspective, P. Degano, R. Gorrieri, A. Marchetti-Spaccamela, and P. Wegner, Eds. Vol. 31. ACM, New York.]]"},{"volume-title":"Proceedings of FSTTCS. Number 2556 in LNCS. Springer-Verlag, 18--32","author":"Miller D.","key":"e_1_2_1_24_1","unstructured":"Miller , D. and Tiu , A . 2002. Encoding generic judgments . In Proceedings of FSTTCS. Number 2556 in LNCS. Springer-Verlag, 18--32 .]] Miller, D. and Tiu, A. 2002. Encoding generic judgments. In Proceedings of FSTTCS. Number 2556 in LNCS. Springer-Verlag, 18--32.]]"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS","author":"Miller D.","year":"2003","unstructured":"Miller , D. and Tiu , A . 2003. A proof theory for generic judgments: An extended abstract . In Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003 ). IEEE, 118--127.]] Miller, D. and Tiu, A. 2003. A proof theory for generic judgments: An extended abstract. In Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003). IEEE, 118--127.]]"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_1_27_1","volume-title":"LFM'02","volume":"70","author":"Momigliano A.","unstructured":"Momigliano , A. , Ambler , S. , and Crole , R . 2002. A hybrid encoding of Howe's method for establishing congruence of bisimilarity . In LFM'02 . ENTCS, vol. 70 .2. Springer-Verlag, New York.]] Momigliano, A., Ambler, S., and Crole, R. 2002. A hybrid encoding of Howe's method for establishing congruence of bisimilarity. In LFM'02. ENTCS, vol. 70.2. Springer-Verlag, New York.]]"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of TYPES 2003 Workshop. Lecture Notes in Computer Science","volume":"3085","author":"Momigliano A.","unstructured":"Momigliano , A. and Tiu , A . 2003. Induction and co-induction in sequent calculus . In Proceedings of TYPES 2003 Workshop. Lecture Notes in Computer Science , vol. 3085 , Springer-Verlag, New York, 293--308.]] Momigliano, A. and Tiu, A. 2003. Induction and co-induction in sequent calculus. In Proceedings of TYPES 2003 Workshop. Lecture Notes in Computer Science, vol. 3085, Springer-Verlag, New York, 293--308.]]"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287599"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00248324"},{"volume-title":"Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation. ACM","author":"Pfenning F.","key":"e_1_2_1_31_1","unstructured":"Pfenning , F. and Elliott , C . 1988. Higher-order abstract syntax . In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation. ACM , New York, 199--208.]] 10.1145\/53990.54010 Pfenning, F. and Elliott, C. 1988. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation. ACM, New York, 199--208.]] 10.1145\/53990.54010"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the 1992 Conference on Automated Deduction. Lecture Notes in Computer Science","volume":"607","author":"Pfenning F.","unstructured":"Pfenning , F. and Rohwedder , E . 1992. Implementing the meta-theory of deductive systems . In Proceedings of the 1992 Conference on Automated Deduction. Lecture Notes in Computer Science , vol. 607 , Springer-Verlag, New York, 537--551.]] Pfenning, F. and Rohwedder, E. 1992. Implementing the meta-theory of deductive systems. In Proceedings of the 1992 Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 607, Springer-Verlag, New York, 537--551.]]"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_2_1_34_1","series-title":"Lecture Notes in Computer Science","volume-title":"Cut-elimination in logics with definitional reflection","author":"Schroeder-Heister P.","unstructured":"Schroeder-Heister , P. 1992. Cut-elimination in logics with definitional reflection . In Nonclassical Logics and Information Processing, D. Pearce and H. Wansing, Eds. Lecture Notes in Computer Science , vol. 619 , Springer-Verlag , New York , 146--171.]] Schroeder-Heister, P. 1992. Cut-elimination in logics with definitional reflection. In Nonclassical Logics and Information Processing, D. Pearce and H. Wansing, Eds. Lecture Notes in Computer Science, vol. 619, Springer-Verlag, New York, 146--171.]]"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the Post-Conference Workshop of ICLP 1994 on Proof-Theoretic Extensions of Logic Programming.]]","author":"Schroeder-Heister P.","year":"1994","unstructured":"Schroeder-Heister , P. 1994 . Cut elimination for logics with definitional reflection and restricted initial sequents . In Proceedings of the Post-Conference Workshop of ICLP 1994 on Proof-Theoretic Extensions of Logic Programming.]] Schroeder-Heister, P. 1994. Cut elimination for logics with definitional reflection and restricted initial sequents. In Proceedings of the Post-Conference Workshop of ICLP 1994 on Proof-Theoretic Extensions of Logic Programming.]]"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00296176"},{"key":"e_1_2_1_38_1","unstructured":"Tiu A. 2004a. Level 0\/1 prover: A tutorial. Available via the web and from Tiu.]]  Tiu A. 2004a. Level 0\/1 prover: A tutorial. Available via the web and from Tiu.]]"},{"volume-title":"Proceedings of the 3rd Workshop on the Foundations of Global Ubiquitous Computing.]]","author":"Tiu A.","key":"e_1_2_1_40_1","unstructured":"Tiu , A. and Miller , D . 2004. A proof search specification of the &pi;-calculus . In Proceedings of the 3rd Workshop on the Foundations of Global Ubiquitous Computing.]] Tiu, A. and Miller, D. 2004. A proof search specification of the &pi;-calculus. In Proceedings of the 3rd Workshop on the Foundations of Global Ubiquitous Computing.]]"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1094622.1094628","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1094622.1094628","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:22:13Z","timestamp":1750278133000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1094622.1094628"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,10]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,10]]}},"alternative-id":["10.1145\/1094622.1094628"],"URL":"https:\/\/doi.org\/10.1145\/1094622.1094628","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2005,10]]},"assertion":[{"value":"2005-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}