{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T23:26:10Z","timestamp":1759879570116},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540436317"},{"type":"electronic","value":"9783540478133"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-47813-2_16","type":"book-chapter","created":{"date-parts":[[2007,5,31]],"date-time":"2007-05-31T02:35:31Z","timestamp":1180578931000},"page":"225-239","source":"Crossref","is-referenced-by-count":6,"title":["An Experiment in Type Inference and Verification by Abstract Interpretation"],"prefix":"10.1007","author":[{"given":"Roberta","family":"Gori","sequence":"first","affiliation":[]},{"given":"Giorgio","family":"Levi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,4,10]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"F. Bourdoncle. Abstract Debugging of Higher-Order Imperative Languages. In Programming Languages Design and Implementation\u2019 93, pages 46\u201355, 1993.","DOI":"10.1145\/155090.155095"},{"key":"16_CR2","unstructured":"F. Bueno, P. Deransart, W. Drabent, G. Ferrand, M. Hermenegildo, J. Maluszynski, and G. Puebla. On the Role of Semantic Approximations in Validation and Diagnosis of Constraint Logic Programs. In M. Kamkar, editor, Proceedings of the AADEBUG\u201997, pages 155\u2013169, 1997."},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"M. Comini, R. Gori, and G. Levi. How to Transform an Analyzer into a Verifier. In R. Nieuwenhuis and A. Voronkov, editors, Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 2250 of Lecture Notes in Artificial Intelligence. Springer-Verlag, Berlin, 2001.","DOI":"10.1007\/3-540-45653-8_41"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"M. Comini, R. Gori, G. Levi, and P. Volpe. Abstract Interpretation based Verification of Logic Programs. In S. Etalle and J.-G. Smaus, editors, Proceedings of the Workshop on Verification of Logic Programs, volume 30 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2000.","DOI":"10.1016\/S1571-0661(04)00112-4"},{"issue":"1","key":"16_CR5","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/S0743-1066(98)10033-X","volume":"39","author":"M. Comini","year":"1999","unstructured":"M. Comini, G. Levi, M. C. Meo, and G. Vitiello. Abstract Diagnosis. Journal of Logic Programming, 39(1\u20133):43\u201393, 1999.","journal-title":"Journal of Logic Programming"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"G. Cousineau and M. Mauny. The Functional Approach to Programming. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139173018"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"P. Cousot. Types as abstract interpretations. In Conference Record of the 24th ACM Symp. on Principles of Programming Languages, pages 316\u2013331. ACM Press, 1997.","DOI":"10.1145\/263699.263744"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proceedings of Fourth ACM Symp. Principles of Programming Languages, pages 238\u2013252, 1977.","DOI":"10.1145\/512950.512973"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Systematic Design of Program Analysis Frameworks. In Proceedings of Sixth ACM Symp. Principles of Programming Languages, pages 269\u2013282, 1979.","DOI":"10.1145\/567752.567778"},{"issue":"4","key":"16_CR10","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"P. Cousot and R. Cousot. Abstract Interpretation Frameworks. Journal of Logic and Computation, 2(4):511\u2013549, 1992.","journal-title":"Journal of Logic and Computation"},{"key":"16_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Comparing the Galois Connection and Widening\/Narrowing Approaches to Abstract Interpretation","author":"P. Cousot","year":"1992","unstructured":"P. Cousot and R. Cousot. Comparing the Galois Connection and Widening\/Narrowing Approaches to Abstract Interpretation. In M. Bruynooghe and M. Wirsing, editors, Proceedings of PLILP\u201992, volume 631 of Lecture Notes in Computer Science, pages 269\u2013295. Springer-Verlag, 1992."},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Inductive Definitions, Semantics and Abstract Interpretation. In Proceedings of Nineteenth Annual ACM Symp. on Principles of Programming Languages, pages 83\u201394. ACM Press, 1992.","DOI":"10.1145\/143165.143184"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"L. Damas and R. Milner. Principal type-schemes for functional programs. In Proceedings of the Ninth Annual ACM Symposium on Principles of Programming Languages, pages 207\u2013212. ACM Press, 1982.","DOI":"10.1145\/582153.582176"},{"issue":"2","key":"16_CR14","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1145\/234528.234742","volume":"28","author":"G. Fil\u00e8","year":"1996","unstructured":"G. Fil\u00e8, R. Giacobazzi, and F. Ranzato. A Unifying View on Abstract Domain Design. ACM Computing Surveys, 28(2):333\u2013336, 1996.","journal-title":"ACM Computing Surveys"},{"key":"16_CR15","doi-asserted-by":"publisher","first-page":"29","DOI":"10.2307\/1995158","volume":"146","author":"J.R. Hindley","year":"1969","unstructured":"J.R. Hindley. The principal type-scheme of an object in combinatory logic. Transaction American mathematical Society, 146:29\u201360, 1969.","journal-title":"Transaction American mathematical Society"},{"key":"16_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/BFb0056610","volume-title":"Derivation of Proof Methods by Abstract Interpretation","author":"G. Levi","year":"1998","unstructured":"G. Levi and P. Volpe. Derivation of Proof Methods by Abstract Interpretation. In C. Palamidessi, H. Glaser, and K. Meinke, editors, Principles of Declarative Programming. 10th International Symposium, PLILP\u201998, volume 1490 of Lecture Notes in Computer Science, pages 102\u2013117. Springer-Verlag, 1998."},{"issue":"3","key":"16_CR17","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"R. Milner. A theory of type polymorphism in programming. Journal of Computer and Systems Sciences, 17-3:348\u2013375, 1978.","journal-title":"Journal of Computer and Systems Sciences"},{"key":"16_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/3-540-56287-7_107","volume-title":"Polymorphic typing by abstract interpretation","author":"B. Monsuez","year":"1992","unstructured":"B. Monsuez. Polymorphic typing by abstract interpretation. In R. Shyamasundar, editor, Proceedings of Foundation of Software Technology and Theoretical Computer Science, volume 652 of Lecture Notes in Computer Science, pages 217\u2013228. Springer-Verlag, 1992."},{"key":"16_CR19","series-title":"Lect Notes Comput Sci","first-page":"224","volume-title":"Polymorphic types and widening operators","author":"B. Monsuez","year":"1993","unstructured":"B. Monsuez. Polymorphic types and widening operators. In P. Cousot, M. Falaschi, G. File', and A. Rauzy, editors, Proceedings of Static Analysis, volume 724 of Lecture Notes in Computer Science, pages 224\u2013281. Springer-Verlag, 1993."},{"key":"16_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/3-540-12925-1_41","volume-title":"Polymorphic type schemes and recursive definitions","author":"A. Mycroft","year":"1984","unstructured":"A. Mycroft. Polymorphic type schemes and recursive definitions. In G. Goos and J. Hartmanis, editors, Proceedings of the International Symposium on Programming, volume 167 of Lecture Notes in Computer Science, pages 217\u2013228. Springer-Verlag, 1984."},{"key":"16_CR21","first-page":"59","volume":"5","author":"D. Park","year":"1969","unstructured":"D. Park. Fixpoint Induction and Proofs of Program Properties. Machine Intelligence, 5:59\u201378, 1969.","journal-title":"Machine Intelligence"},{"issue":"1","key":"16_CR22","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1002\/(SICI)1096-9942(1998)4:1<27::AID-TAPO3>3.0.CO;2-4","volume":"4","author":"D. R\u00e9my","year":"1998","unstructured":"D. R\u00e9my and J. Vouillon. Objective ML:An effective object-oriented extension to ML. Theory and Practice of Object-Systems, 4(1):27\u201350, 1998.","journal-title":"Theory and Practice of Object-Systems"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-47813-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T13:36:15Z","timestamp":1556458575000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-47813-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540436317","9783540478133"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-47813-2_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}