{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T11:19:33Z","timestamp":1725621573977},"publisher-location":"New York, NY, USA","reference-count":9,"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.1088460","type":"proceedings-article","created":{"date-parts":[[2005,11,7]],"date-time":"2005-11-07T17:34:39Z","timestamp":1131384879000},"page":"41-49","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Translating specifications from nominal logic to CIC with the theory of contexts"],"prefix":"10.1145","author":[{"given":"Marino","family":"Miculan","sequence":"first","affiliation":[{"name":"University of Udine, Udine, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ivan","family":"Scagnetto","sequence":"additional","affiliation":[{"name":"University of Udine, Udine, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Furio","family":"Honsell","sequence":"additional","affiliation":[{"name":"University of Udine, Udine, Italy"}],"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-31982-5_24"},{"key":"e_1_3_2_1_2_1","first-page":"193","volume-title":"Proc. 14th LICS","author":"Fiore M. P.","year":"1999","unstructured":"M. P. Fiore , G. D. Plotkin , and D. Turi . Abstract syntax and variable binding . In G. Longo, editor, Proc. 14th LICS , pages 193 -- 202 , Trento, Italy , 1999 . IEEE Computer Society Press .]] M. P. Fiore, G. D. Plotkin, and D. Turi. Abstract syntax and variable binding. In G. Longo, editor, Proc. 14th LICS, pages 193--202, Trento, Italy, 1999. IEEE Computer Society Press.]]"},{"key":"e_1_3_2_1_3_1","volume-title":"Fresh logic: a logic of FM. Submitted","author":"Gabbay M. J.","year":"2003","unstructured":"M. J. Gabbay . Fresh logic: a logic of FM. Submitted , 2003 .]] M. J. Gabbay. Fresh logic: a logic of FM. Submitted, 2003.]]"},{"key":"e_1_3_2_1_4_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"963","DOI":"10.1007\/3-540-48224-5_78","volume-title":"Proc. ICALP'01","author":"Honsell F.","year":"2001","unstructured":"F. Honsell , M. Miculan , and I. Scagnetto . An axiomatic approach to metareasoning on systems in higher-order abstract syntax . In Proc. ICALP'01 , volume 2076 of Lecture Notes in Computer Science , pages 963 -- 978 . Springer , 2001 .]] F. Honsell, M. Miculan, and I. Scagnetto. An axiomatic approach to metareasoning on systems in higher-order abstract syntax. In Proc. ICALP'01, volume 2076 of Lecture Notes in Computer Science, pages 963--978. Springer, 2001.]]"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00095-5"},{"key":"e_1_3_2_1_6_1","volume-title":"The Coq Proof Assistant, version 8","author":"INRIA.","year":"2004","unstructured":"INRIA. The Coq Proof Assistant, version 8 , 2004 . Available at http:\/\/coq.inria.fr\/doc\/main.html .]] INRIA. The Coq Proof Assistant, version 8, 2004. Available at http:\/\/coq.inria.fr\/doc\/main.html .]]"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/333580.333590"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/788023.789055"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"}],"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.1088460","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T14:16:41Z","timestamp":1673446601000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1088454.1088460"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,9,27]]},"references-count":9,"alternative-id":["10.1145\/1088454.1088460","10.1145\/1088454"],"URL":"https:\/\/doi.org\/10.1145\/1088454.1088460","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"}}]}}