{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T18:33:22Z","timestamp":1730313202245,"version":"3.28.0"},"publisher-location":"New York, NY, USA","reference-count":13,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2005,9,27]]},"DOI":"10.1145\/1088454.1088461","type":"proceedings-article","created":{"date-parts":[[2005,11,7]],"date-time":"2005-11-07T17:34:39Z","timestamp":1131384879000},"page":"50-57","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Types with semantics"],"prefix":"10.1145","author":[{"given":"Olha","family":"Shkaravska","sequence":"first","affiliation":[{"name":"Ludwig-Maximilians University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,9,27]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_1"},{"key":"e_1_3_2_1_2_1","first-page":"34","volume-title":"Proceedings of 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs2004)","author":"Beringer L.","year":"2004","unstructured":"Beringer , L. , Hofmann , M. , Loidl , H.-W. , and Momigliano , A . A Program Logic for Resource Verification . In Proceedings of 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs2004) , pages 34 -- 49 . Springer-Verlag LNCS , September 2004 . Beringer, L., Hofmann, M., Loidl, H.-W., and Momigliano, A. A Program Logic for Resource Verification. In Proceedings of 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs2004), pages 34--49. Springer-Verlag LNCS, September 2004."},{"key":"e_1_3_2_1_3_1","first-page":"347","volume-title":"Artificial Intelligence and Reasoning: 11th International Conference, LPAR 2004","volume":"3452","author":"Beringer L.","year":"2005","unstructured":"Beringer , L. , Hofmann , M. , Momigliano , A. , and Shkaravska , O . Automatic Certification of Heap Consumption. In Logic for Programming , Artificial Intelligence and Reasoning: 11th International Conference, LPAR 2004 , volume 3452 , pages 347 -- 362 . Springer-Verlag , 2005 . Beringer, L., Hofmann, M., Momigliano, A., and Shkaravska, O. Automatic Certification of Heap Consumption. In Logic for Programming, Artificial Intelligence and Reasoning: 11th International Conference, LPAR 2004, volume 3452, pages 347--362. Springer-Verlag, 2005."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_3"},{"key":"e_1_3_2_1_6_1","volume-title":"Mobile Resource Guarantee Project Deliverable D2e","author":"Beringer L.","year":"2003","unstructured":"Beringer , L. , and Momigliano , A . Implement a theorem prover . In Mobile Resource Guarantee Project Deliverable D2e , November 2003 . Beringer, L., and Momigliano, A. Implement a theorem prover. In Mobile Resource Guarantee Project Deliverable D2e, November 2003."},{"key":"e_1_3_2_1_7_1","volume-title":"A Gentle Introduction to Camelot","author":"Loidl H.-W.","year":"2004","unstructured":"Loidl , H.-W. , and MacKenzie , K. A Gentle Introduction to Camelot . September , 2004 . http:\/\/groups.inf.ed.ac.uk\/mrg\/camelot\/Gentle-Camelot\/camelot-gentle-intro.html. Loidl, H.-W., and MacKenzie, K. A Gentle Introduction to Camelot. September, 2004. http:\/\/groups.inf.ed.ac.uk\/mrg\/camelot\/Gentle-Camelot\/camelot-gentle-intro.html."},{"key":"e_1_3_2_1_8_1","first-page":"29","volume-title":"Trends in Functional Programming","volume":"4","author":"MacKenzie K.","year":"2004","unstructured":"MacKenzie , K. , and Wolverson , N . Camelot and Grail: resource-aware functional programming on the JVM . In Trends in Functional Programming , volume 4 , pages 29 -- 46 . Intellect , 2004 . MacKenzie, K., and Wolverson, N. Camelot and Grail: resource-aware functional programming on the JVM. In Trends in Functional Programming, volume 4, pages 29--46. Intellect, 2004."},{"key":"e_1_3_2_1_9_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/978-3-540-30142-4_22","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs","author":"Wildmoser M.","year":"2004","unstructured":"Wildmoser , M. , and Nipkow , T . Certifying Machine Code Safety: Shallow versus Deep Embedding . In K. Slind and A. Bunker and G. Gopalakrishnan, editors, Theorem Proving in Higher Order Logics (TPHOLs 2004 , volume 3223 of LNCS , pages 305 -- 320 . Springer , 2004. Wildmoser, M., and Nipkow, T. Certifying Machine Code Safety: Shallow versus Deep Embedding. In K. Slind and A. Bunker and G. Gopalakrishnan, editors, Theorem Proving in Higher Order Logics (TPHOLs 2004, volume 3223 of LNCS, pages 305--320. Springer, 2004."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_1_11_1","volume-title":"A Program Logic for Resource. Submitted","author":"Aspinall D.","year":"2005","unstructured":"Aspinall , D. , Beringer , L. , Hofmann , M. , Loidl , H.-W. , and Momigliano , A . A Program Logic for Resource. Submitted , 2005 . Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., and Momigliano, A. A Program Logic for Resource. Submitted, 2005."},{"key":"e_1_3_2_1_12_1","first-page":"36","volume-title":"Another Type System for In-Place Update. In ESOP'02 --- European Symposium on Programming, LNCS 2305","author":"Aspinall D.","year":"2002","unstructured":"Aspinall , D. , and Hofmann , M . Another Type System for In-Place Update. In ESOP'02 --- European Symposium on Programming, LNCS 2305 , pages 36 - 52 , Springer , 2002 . Aspinall, D., and Hofmann, M. Another Type System for In-Place Update. In ESOP'02 --- European Symposium on Programming, LNCS 2305, pages 36-52, Springer, 2002."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"}],"event":{"name":"MERLIN05: Mechanized Reasoning about Languages with Variable Binding 2005 Workshop","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"],"location":"Tallinn Estonia","acronym":"MERLIN05"},"container-title":["Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1088454.1088461","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T14:16:49Z","timestamp":1673446609000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1088454.1088461"}},"subtitle":["soundness proof assistant"],"short-title":[],"issued":{"date-parts":[[2005,9,27]]},"references-count":13,"alternative-id":["10.1145\/1088454.1088461","10.1145\/1088454"],"URL":"https:\/\/doi.org\/10.1145\/1088454.1088461","relation":{},"subject":[],"published":{"date-parts":[[2005,9,27]]},"assertion":[{"value":"2005-09-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}