{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,14]],"date-time":"2023-01-14T00:14:47Z","timestamp":1673655287124},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2011,6,1]],"date-time":"2011-06-01T00:00:00Z","timestamp":1306886400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2011,6]]},"DOI":"10.1007\/s10990-011-9071-2","type":"journal-article","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T12:55:48Z","timestamp":1308401748000},"page":"41-80","source":"Crossref","is-referenced-by-count":2,"title":["Logical approximation for program analysis"],"prefix":"10.1007","volume":"24","author":[{"given":"Robert J.","family":"Simmons","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,6,19]]},"reference":[{"key":"9071_CR1","volume-title":"Compilers: Principles, Techniques and Tools","author":"A.V. Aho","year":"2007","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques and Tools, 2nd edn. Pearson Education, Upper Saddle River (2007)","edition":"2"},{"issue":"3","key":"9071_CR2","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J.M. Andreoli","year":"1992","unstructured":"Andreoli, J.M.: Logic programming with focusing proofs in linear logic. J. Log. Comput. 2(3), 297\u2013347 (1992)","journal-title":"J. Log. Comput."},{"key":"9071_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/3-540-45744-5_21","volume-title":"International Joint Conference on Automated Reasoning","author":"P. Armel\u00edn","year":"2001","unstructured":"Armel\u00edn, P., Pym, D.: Bunched logic programming. In: International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science, vol. 2083, pp. 289\u2013304. Springer, New York (2001)"},{"key":"9071_CR4","unstructured":"Barber, A.: Dual intuitionistic linear logic. Tech. Rep. ECS-LFCS-96-347, Laboratory for Foundations of Computer Sciences, University of Edinburgh (1996)"},{"key":"9071_CR5","series-title":"Studies in Logic and the Foundations of Mathematics","first-page":"225","volume-title":"Language in Action: Categories, Lambdas and Dynamic Logic","author":"J. Benthem van","year":"1991","unstructured":"van Benthem, J.: Language in Action: Categories, Lambdas and Dynamic Logic. Studies in Logic and the Foundations of Mathematics, vol.\u00a0130, pp. 225\u2013250. North-Holland, Amsterdam (1991). Chap. 16"},{"key":"9071_CR6","first-page":"38","volume-title":"International Conference on Principles and Practice of Declarative Programming","author":"M. Bozzano","year":"2002","unstructured":"Bozzano, M., Delzanno, G.: Automated protocol verification in linear logic. In: International Conference on Principles and Practice of Declarative Programming, pp. 38\u201349. ACM, New York (2002)"},{"issue":"1","key":"9071_CR7","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1017\/S1471068402001254","volume":"2","author":"M. Bozzano","year":"2002","unstructured":"Bozzano, M., Delzanno, G., Martelli, M.: An effective fixpoint semantics for linear logic programs. Theory Pract. Log. Program. 2(1), 85\u2013122 (2002)","journal-title":"Theory Pract. Log. Program."},{"issue":"5\u20136","key":"9071_CR8","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1017\/S1471068404002066","volume":"4","author":"M. Bozzano","year":"2004","unstructured":"Bozzano, M., Delzanno, G., Martelli, M.: Model checking linear logic specifications. Theory Pract. Log. Program. 4(5\u20136), 573\u2013619 (2004)","journal-title":"Theory Pract. Log. Program."},{"key":"9071_CR9","first-page":"243","volume-title":"Object-Oriented Programming, Systems, Languages, and Applications","author":"M. Bravenboer","year":"2009","unstructured":"Bravenboer, M., Smaragdakis, Y.: Strictly declarative specification of sophisticated points-to analyses. In: Object-Oriented Programming, Systems, Languages, and Applications, pp. 243\u2013261. ACM, New York (2009)"},{"key":"9071_CR10","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1142\/9781848161023_0010","volume-title":"Coordination Programming: Mechanisms, Models and Semantics","author":"P. Bruscoli","year":"1996","unstructured":"Bruscoli, P., Guglielmi, A.: A linear logic view of Gamma style computations as proof searches. In: Andreoli, J.M., Hankin, C., M\u00e9tayer, D.L. (eds.) Coordination Programming: Mechanisms, Models and Semantics, pp. 249\u2013273. Imperial College Press, London (1996)"},{"key":"9071_CR11","unstructured":"Cervesato, I., Pfenning, F., Walker, D., Watkins, K.: A concurrent logical framework II: Examples and applications. Tech. Rep. CMU-CS-02-102, School of Computer Science, Carnegie Mellon University (2002). Revised May 2003"},{"key":"9071_CR12","doi-asserted-by":"crossref","first-page":"1044","DOI":"10.1016\/j.ic.2008.11.006","volume":"207","author":"I. Cervesato","year":"2009","unstructured":"Cervesato, I., Scedrov, A.: Relating state-based and process-based concurrency through linear logic. Inf. Comput. 207, 1044\u20131077 (2009)","journal-title":"Inf. Comput."},{"key":"9071_CR13","first-page":"238","volume-title":"Symposium on Principles of Programming Languages","author":"P. Cousout","year":"1977","unstructured":"Cousout, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM, New York (1977)"},{"key":"9071_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/3-540-45619-8_15","volume-title":"International Conference on Logic Programming","author":"H. Ganzinger","year":"2002","unstructured":"Ganzinger, H., McAllester, D.A.: Logical algorithms. In: International Conference on Logic Programming. Lecture Notes in Computer Science, vol. 2401, pp. 209\u2013223. Springer, New York (2002)"},{"key":"9071_CR15","unstructured":"Girard, J.Y.: A fixpoint theorem in linear logic (1992). An email posting to the mailing list linear@cs.stanford.edu"},{"issue":"2","key":"9071_CR16","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1006\/inco.1994.1036","volume":"110","author":"J.S. Hodas","year":"1994","unstructured":"Hodas, J.S., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Inf. Comput. 110(2), 327\u2013365 (1994)","journal-title":"Inf. Comput."},{"key":"9071_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1007\/11590156_42","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"R. Jagadeesan","year":"2005","unstructured":"Jagadeesan, R., Nadathur, G., Saraswat, V.A.: Testing concurrent systems: an interpretation of intuitionistic logic. In: Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science, vol. 3821, pp. 517\u2013528. Springer, New York (2005)"},{"key":"9071_CR18","first-page":"1","volume-title":"Principles of Database Systems","author":"M.S. Lam","year":"2005","unstructured":"Lam, M.S., Whaley, J., Livshits, V.B., Martin, M.C., Avots, D., Carbin, M., Unkel, C.: Context-sensitive program analysis as database queries. In: Principles of Database Systems, pp. 1\u201312. ACM, New York (2005)"},{"key":"9071_CR19","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1080\/00029890.1958.11989160","volume":"65","author":"J. Lambek","year":"1958","unstructured":"Lambek, J.: The mathematics of sentence structure. Am. Math. Mon. 65, 363\u2013386 (1958)","journal-title":"Am. Math. Mon."},{"key":"9071_CR20","first-page":"35","volume-title":"Principles and Practice of Declarative Programming","author":"P. L\u00f3pez","year":"2005","unstructured":"L\u00f3pez, P., Pfenning, F., Polakow, J., Watkins, K.: Monadic concurrent linear logic programming. In: Principles and Practice of Declarative Programming, pp. 35\u201346. ACM, New York (2005)"},{"issue":"4","key":"9071_CR21","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1145\/581771.581774","volume":"49","author":"D.A. McAllester","year":"2002","unstructured":"McAllester, D.A.: On the complexity analysis of static analyses. J. ACM 49(4), 512\u2013537 (2002)","journal-title":"J. ACM"},{"key":"9071_CR22","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1016\/j.tcs.2006.12.018","volume":"373","author":"J. Meseguer","year":"2007","unstructured":"Meseguer, J., Ro\u015fu, G.: The rewriting logic semantics project. Theor. Comput. Sci. 373, 213\u2013237 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"9071_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/978-3-642-15769-1_25","volume-title":"Static Analysis Symposium","author":"M. Might","year":"2010","unstructured":"Might, M.: Abstract interpreters for free. In: Static Analysis Symposium. Lecture Notes in Computer Science, vol. 6337, pp. 407\u2013421. Springer, New York (2010)"},{"key":"9071_CR24","first-page":"305","volume-title":"Programming Language Design and Implementation","author":"M. Might","year":"2010","unstructured":"Might, M., Smaragdakis, Y., Van Horn, D.: Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis. In: Programming Language Design and Implementation, pp. 305\u2013315. ACM, New York (2010)"},{"issue":"4","key":"9071_CR25","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. Log. Comput. 1(4), 497\u2013536 (1991)","journal-title":"J. Log. Comput."},{"issue":"1","key":"9071_CR26","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/0304-3975(96)00045-X","volume":"165","author":"D. Miller","year":"1996","unstructured":"Miller, D.: A multiple-conclusion meta-logic. Theor. Comput. Sci. 165(1), 201\u2013232 (1996)","journal-title":"Theor. Comput. Sci."},{"key":"9071_CR27","series-title":"Studies in Logic","first-page":"423","volume-title":"Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday","author":"D. Miller","year":"2008","unstructured":"Miller, D.: A proof-theoretic approach to the static analysis of logic programs. In: Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday. Studies in Logic, vol. 17, pp. 423\u2013442. College Publications, London (2008)"},{"issue":"1\u20132","key":"9071_CR28","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Log. 51(1\u20132), 125\u2013157 (1991)","journal-title":"Ann. Pure Appl. Log."},{"issue":"2","key":"9071_CR29","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1023\/A:1008399708659","volume":"10","author":"R. Moot","year":"2001","unstructured":"Moot, R., Piazza, M.: Linguistic applications of first order intuitionistic linear logic. J. Log. Lang. Inf. 10(2), 211\u2013232 (2001)","journal-title":"J. Log. Lang. Inf."},{"key":"9071_CR30","first-page":"133","volume-title":"Proceedings of the Meeting of the European Chapter of the Association for Computational Linguistics","author":"G. Morrill","year":"1995","unstructured":"Morrill, G.: Higher-order linear logic programming of categorial deduction. In: Proceedings of the Meeting of the European Chapter of the Association for Computational Linguistics, pp. 133\u2013140. Morgan Kaufmann, San Mateo (1995)"},{"key":"9071_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/978-3-540-30477-7_13","volume-title":"Asian Symposium on Programming Languages and Systems","author":"F. Pfenning","year":"2004","unstructured":"Pfenning, F.: Substructural operational semantics and linear destination-passing style. In: Asian Symposium on Programming Languages and Systems. Lecture Notes in Computer Science, vol. 3302, p. 196. Springer, New York (2004). Abstract of invited talk"},{"key":"9071_CR32","first-page":"199","volume-title":"Programming Language Design and Implementation","author":"F. Pfenning","year":"1988","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Programming Language Design and Implementation, pp. 199\u2013208. ACM, New York (1988)"},{"key":"9071_CR33","series-title":"Lecture Notes in Computer Science","first-page":"179","volume-title":"Types for Proofs and Programs","author":"F. Pfenning","year":"1998","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: Algorithms for equality and unification in the presence of notational definitions. In: Types for Proofs and Programs. Lecture Notes in Computer Science, vol. 1657, pp. 179\u2013193. Springer, New York (1998)"},{"key":"9071_CR34","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1109\/LICS.2009.8","volume-title":"Symposium on Logic in Computer Science","author":"F. Pfenning","year":"2009","unstructured":"Pfenning, F., Simmons, R.J.: Substructural operational semantics as ordered logic programming. In: Symposium on Logic in Computer Science, pp. 101\u2013110. IEEE Computer Society Press, Los Alamitos (2009)"},{"key":"9071_CR35","first-page":"17","volume":"60\u201361","author":"G.D. Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60\u201361, 17\u2013139 (2004). Reprinted with corrections from Aarhus University technical report DAIMI FN-19","journal-title":"J. Log. Algebr. Program."},{"key":"9071_CR36","first-page":"68","volume-title":"International Conference on Principles and Practice of Declarative Programming","author":"J. Polakow","year":"2000","unstructured":"Polakow, J.: Linear logic programming with an ordered context. In: International Conference on Principles and Practice of Declarative Programming, pp. 68\u201379. ACM, New York (2000)"},{"key":"9071_CR37","unstructured":"Polakow, J.: Ordered linear logic and applications. PhD thesis, Carnegie Mellon University (2001). Available as technical report CMU-CS-01-152"},{"key":"9071_CR38","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. Journal of Logic and Algebraic Programming 79(6) (2010)","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"9071_CR39","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1023\/A:1022678217288","volume":"14","author":"C. Rouveirol","year":"1994","unstructured":"Rouveirol, C.: Flattening and saturation: two representation changes for generalization. Mach. Learn. 14, 219\u2013232 (1994)","journal-title":"Mach. Learn."},{"key":"9071_CR40","first-page":"222","volume-title":"Symposium on Logic and Computer Science","author":"P. Schroeder-Heister","year":"1993","unstructured":"Schroeder-Heister, P.: Rules of definitional reflection. In: Symposium on Logic and Computer Science, pp. 222\u2013232. IEEE Computer Society Press, Los Alamitos (1993)"},{"key":"9071_CR41","unstructured":"Sch\u00fcrmann, C.: Automating the meta theory of deductive systems. PhD thesis, Carnegie Mellon University (2000). Available as Technical Report CMU-CS-00-146"},{"key":"9071_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1007\/978-3-642-16310-4_8","volume-title":"Rewriting Logic and Its Applications","author":"T.F. \u015eerb\u0103nu\u0163\u0103","year":"2010","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: K-Maude: a rewriting based tool for semantics of programming languages. In: Rewriting Logic and Its Applications. Lecture Notes in Computer Science, vol. 6381, pp. 104\u2013122. Springer, New York (2010)"},{"issue":"1\u20132","key":"9071_CR43","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0743-1066(95)00035-I","volume":"24","author":"S.M. Shieber","year":"1995","unstructured":"Shieber, S.M., Schabes, Y., Pereira, F.C.N.: Principles and implementation of deductive parsing. J. Log. Program. 24(1\u20132), 3\u201336 (1995)","journal-title":"J. Log. Program."},{"key":"9071_CR44","unstructured":"Simmons, R.J.: Type safety for substructural specifications: preliminary results. Tech. Rep. CMU-CS-10-134, School of Computer Science, Carnegie Mellon University (2010)"},{"key":"9071_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1007\/978-3-540-70583-3_28","volume-title":"International Colloquium on Automata, Languages and Programming","author":"R.J. Simmons","year":"2008","unstructured":"Simmons, R.J., Pfenning, F.: Linear logical algorithms. In: International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 5126, pp. 336\u2013345. Springer, New York (2008)"},{"key":"9071_CR46","first-page":"9","volume-title":"Partial Evaluation and Program Manipulation","author":"R.J. Simmons","year":"2009","unstructured":"Simmons, R.J., Pfenning, F.: Linear logical approximations. In: Partial Evaluation and Program Manipulation, pp. 9\u201320. ACM, New York (2009)"},{"key":"9071_CR47","unstructured":"Simmons, R.J., Pfenning, F.: Weak focusing for ordered linear logic. Tech. Rep. CMU-CS-10-147, School of Computer Science, Carnegie Mellon University (2011)"},{"key":"9071_CR48","first-page":"85","volume-title":"International Conference on Functional Programming","author":"D. Horn Van","year":"2007","unstructured":"Van Horn, D., Mairson, H.G.: Relating complexity and precision in control flow analysis. In: International Conference on Functional Programming, pp. 85\u201396. ACM, New York (2007)"},{"key":"9071_CR49","first-page":"51","volume-title":"International Conference on Functional Programming","author":"D. Horn Van","year":"2010","unstructured":"Van Horn, D., Might, M.: Abstracting abstract machines. In: International Conference on Functional Programming, pp. 51\u201362. ACM, New York (2010)"},{"key":"9071_CR50","unstructured":"Virga, R.: Higher-order rewriting with dependent types. PhD thesis, Carnegie Mellon University (1999)"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-011-9071-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-011-9071-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-011-9071-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T00:15:36Z","timestamp":1560298536000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-011-9071-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,6]]},"references-count":50,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2011,6]]}},"alternative-id":["9071"],"URL":"https:\/\/doi.org\/10.1007\/s10990-011-9071-2","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,6]]}}}