{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:25:35Z","timestamp":1781893535545,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642358722","type":"print"},{"value":"9783642358739","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-35873-9_19","type":"book-chapter","created":{"date-parts":[[2013,1,2]],"date-time":"2013-01-02T06:22:57Z","timestamp":1357107777000},"page":"295-314","source":"Crossref","is-referenced-by-count":27,"title":["Compositional and Lightweight Dependent Type Inference for ML"],"prefix":"10.1007","author":[{"given":"He","family":"Zhu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-540-73368-3_41","volume-title":"Computer Aided Verification","author":"D. Babi\u0107","year":"2007","unstructured":"Babi\u0107, D., Hu, A.J.: Structural Abstraction of Software Verification Conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 366\u2013378. Springer, Heidelberg (2007)"},{"key":"19_CR2","unstructured":"Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: Static Driver Verification with Under 4% False Alarms. In: FMCAD, pp. 35\u201342 (2010)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"19_CR4","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The Software Model Checker Blast: Applications to Software Engineering. Int. J. Softw. Tools Technol. Transf.\u00a09, 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-540-70545-1_29","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2008","unstructured":"Beyer, D., Zufferey, D., Majumdar, R.: cSIsat: Interpolation for LA+EUF. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 304\u2013308. Springer, Heidelberg (2008)"},{"key":"19_CR6","unstructured":"http:\/\/www.lri.fr\/~filliatr\/software.en.html"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Damas, L., Milner, R.: Principal Type-Schemes for Functional Programs. In: POPL, pp. 207\u2013212 (1982)","DOI":"10.1145\/582153.582176"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI, pp. 234\u2013245 (2002)","DOI":"10.1145\/543552.512558"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Freeman, T., Pfenning, F.: Refinement Types for ML. In: PLDI, pp. 268\u2013277 (1991)","DOI":"10.1145\/113446.113468"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Jagannathan, S., Weeks, S.: A Unified Treatment of Flow Analysis in Higher-Order Languages. In: POPL, pp. 393\u2013407 (1995)","DOI":"10.1145\/199448.199536"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-642-22110-1_38","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2011","unstructured":"Jhala, R., Majumdar, R., Rybalchenko, A.: HMC: Verifying Functional Programs Using Abstract Interpreters. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 470\u2013485. Springer, Heidelberg (2011)"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Kawaguci, M., Rondon, P., Jhala, R.: Type-based Data Structure Verification. In: PLDI, pp. 304\u2013315 (2009)","DOI":"10.1145\/1543135.1542510"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/978-3-540-71316-6_34","volume-title":"Programming Languages and Systems","author":"K. Knowles","year":"2007","unstructured":"Knowles, K., Flanagan, C.: Type Reconstruction for General Refinement Types. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 505\u2013519. Springer, Heidelberg (2007)"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Model-Checking Higher-Order Functions. In: PPDP, pp. 25\u201336 (2009)","DOI":"10.1145\/1599410.1599415"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs. In: POPL, pp. 416\u2013428 (2009)","DOI":"10.1145\/1594834.1480933"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate Abstraction and CEGAR for Higher-Order Model Checking. In: PLDI, pp. 222\u2013233 (2011)","DOI":"10.1145\/1993316.1993525"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification. In: POPL, pp. 495\u2013508 (2010)","DOI":"10.1145\/1707801.1706355"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: Constructive Mathematics and Computer Programming (312), 501\u2013518 (1984)","DOI":"10.1098\/rsta.1984.0073"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Ong, C.H.L., Ramsay, S.J.: Verifying Higher-Order Functional Programs with Pattern-Matching Algebraic Data Types. In: POPL, pp. 587\u2013598 (2011)","DOI":"10.1145\/1925844.1926453"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Rondon, P., Kawaguci, M., Jhala, R.: Liquid Types. In: PLDI, pp. 159\u2013169 (2008)","DOI":"10.1145\/1379022.1375602"},{"key":"19_CR24","unstructured":"Sharir, M., Pnueli, A.: Two Approaches to Interprocedural Data Flow Analysis. In: Program Flow Analysis (1981)"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Shivers, O.: Control-Flow analysis in Scheme. In: PLDI, pp. 164\u2013174 (1988)","DOI":"10.1145\/960116.54007"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Terauchi, T.: Dependent types from Counterexamples. In: POPL, pp. 119\u2013130 (2010)","DOI":"10.1145\/1707801.1706315"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Unno, H., Kobayashi, N.: Dependent Type Inference with Interpolants. In: PPDP, pp. 277\u2013288 (2009)","DOI":"10.1145\/1599410.1599445"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Dependent Types in Practical Programming. In: POPL, pp. 214\u2013227 (1999)","DOI":"10.1145\/292540.292560"}],"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\/978-3-642-35873-9_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T13:32:52Z","timestamp":1620135172000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35873-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642358722","9783642358739"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35873-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}