{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:52:04Z","timestamp":1790927524338,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,10,30]],"date-time":"2016-10-30T00:00:00Z","timestamp":1477785600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001711","name":"Schweizerischer Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","doi-asserted-by":"publisher","award":["200020_159949, IZ74Z0_160453"],"award-info":[{"award-number":["200020_159949, IZ74Z0_160453"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["306484 - IMPRO"],"award-info":[{"award-number":["306484 - IMPRO"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,10,30]]},"DOI":"10.1145\/2998392.2998398","type":"proceedings-article","created":{"date-parts":[[2016,10,21]],"date-time":"2016-10-21T14:16:42Z","timestamp":1477059402000},"page":"31-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["SMT-based checking of predicate-qualified types for Scala"],"prefix":"10.1145","author":[{"given":"Georg Stefan","family":"Schmid","sequence":"first","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2016,10,30]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions","author":"Bertot Y.","year":"2010","unstructured":"Y. Bertot and P. Castran . Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions . Springer , 1 st edition, 2010 . Y. Bertot and P. Castran. Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions. Springer, 1st edition, 2010.","edition":"1"},{"key":"e_1_3_2_1_2_1","unstructured":"ISBN 3642058809 9783642058806.  ISBN 3642058809 9783642058806."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2774975.2774980"},{"key":"e_1_3_2_1_4_1","volume-title":"Extra - Read All About It: Nearly All Binary Searches and Mergesorts are Broken. https:\/\/research.googleblog.com\/2006\/06\/ extra-extra-read-all-about-it-nearly.html","author":"Bloch J.","year":"2006","unstructured":"J. Bloch . Extra , Extra - Read All About It: Nearly All Binary Searches and Mergesorts are Broken. https:\/\/research.googleblog.com\/2006\/06\/ extra-extra-read-all-about-it-nearly.html , 2006 . Accessed : 2016-06-23. J. Bloch. Extra, Extra - Read All About It: Nearly All Binary Searches and Mergesorts are Broken. https:\/\/research.googleblog.com\/2006\/06\/ extra-extra-read-all-about-it-nearly.html, 2006. Accessed: 2016-06-23."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_1_6_1","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable R. L.","year":"1986","unstructured":"R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , and S. F. Smith . Implementing Mathematics with the Nuprl Proof Development System . Prentice-Hall, Inc. , 1986 . ISBN 0-13-451832-2. R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Inc., 1986. ISBN 0-13-451832-2."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_2_1_8_1","volume-title":"Oracle","author":"Gosling J.","year":"2015","unstructured":"J. Gosling , B. Joy , G. Steele , G. Bracha , and A. Buckley . The Java R Language Specification (Java SE 8 Edition) . Oracle , 2015 . J. Gosling, B. Joy, G. Steele, G. Bracha, and A. Buckley. The Java R Language Specification (Java SE 8 Edition). Oracle, 2015."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509555"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A generic theorem prover","author":"Paulson L. C.","year":"1994","unstructured":"L. C. Paulson . Isabelle: A generic theorem prover , volume 828 . Springer , 1994 . L. C. Paulson. Isabelle: A generic theorem prover, volume 828. Springer, 1994."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268967"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-014-0219-7"},{"key":"e_1_3_2_1_15_1","unstructured":"F. S. Thomas. Refined \u2013 Simple refinement types for Scala. http:\/\/refined.timepit.eu 2016. Accessed: 2016-06- 23.  F. S. Thomas. Refined \u2013 Simple refinement types for Scala. http:\/\/refined.timepit.eu 2016. Accessed: 2016-06- 23."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"}],"event":{"name":"SPLASH '16: Conference on Systems, Programming, Languages, and Applications: Software for Humanity","location":"Amsterdam Netherlands","acronym":"SPLASH '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGAda ACM Special Interest Group on Ada Programming Language"]},"container-title":["Proceedings of the 2016 7th ACM SIGPLAN Symposium on Scala"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2998392.2998398","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2998392.2998398","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:50:34Z","timestamp":1750218634000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2998392.2998398"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,30]]},"references-count":16,"alternative-id":["10.1145\/2998392.2998398","10.1145\/2998392"],"URL":"https:\/\/doi.org\/10.1145\/2998392.2998398","relation":{},"subject":[],"published":{"date-parts":[[2016,10,30]]},"assertion":[{"value":"2016-10-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}