{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:12Z","timestamp":1750220652145,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":18,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,19]],"date-time":"2020-10-19T00:00:00Z","timestamp":1603065600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Secretaria de Ciencia y Tecnolog\u00eda - Universidad Nacional de C\u00f3rdoba","award":["Certificaci\u00f3n de Compilador hacia ARM"],"award-info":[{"award-number":["Certificaci\u00f3n de Compilador hacia ARM"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,10,19]]},"DOI":"10.1145\/3427081.3427086","type":"proceedings-article","created":{"date-parts":[[2020,10,22]],"date-time":"2020-10-22T23:50:55Z","timestamp":1603410655000},"page":"33-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A formalisation of LEGv8 in Agda"],"prefix":"10.1145","author":[{"given":"Santiago Arranz","family":"Olmos","sequence":"first","affiliation":[{"name":"FAMAF - Universidad Nacional de C\u00f3rdoba"}]},{"given":"Mart\u00edn","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[{"name":"FAMAF - Universidad Nacional de C\u00f3rdoba"}]},{"given":"Mat\u00edas","family":"Steinberg","sequence":"additional","affiliation":[{"name":"FAMAF - Universidad Nacional de C\u00f3rdoba"}]},{"given":"Alejandro","family":"Gadea","sequence":"additional","affiliation":[{"name":"FAMAF - Universidad Nacional de C\u00f3rdoba"}]},{"given":"Emmanuel","family":"Gunther","sequence":"additional","affiliation":[{"name":"FAMAF - Universidad Nacional de C\u00f3rdoba"}]},{"given":"Miguel","family":"Pagano","sequence":"additional","affiliation":[{"name":"FAMAF - Universidad Nacional de C\u00f3rdoba"}]}],"member":"320","published-online":{"date-parts":[[2020,10,22]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481839.1481842"},{"volume-title":"ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile) (DDI0487)","author":"Ltd ARM","key":"e_1_3_2_1_2_1","unstructured":"ARM Ltd . 2017. ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile) (DDI0487) . ARM Ltd . https:\/\/developer.arm.com\/docs\/ddi0487\/a\/arm-architecture- reference- manual- armv8-for-armv8-a-architecture-profile ARM Ltd. 2017. ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile) (DDI0487). ARM Ltd. https:\/\/developer.arm.com\/docs\/ddi0487\/a\/arm-architecture- reference- manual- armv8-for-armv8-a-architecture-profile"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796815000180"},{"key":"e_1_3_2_1_4_1","volume-title":"Calculating Correct Compilers II: Return of the Register Machines. Journal of Functional Programming","author":"Bahr Patrick","year":"2020","unstructured":"Patrick Bahr and Graham Hutton . 2020. Calculating Correct Compilers II: Return of the Register Machines. Journal of Functional Programming ( 2020 ). To appear. Patrick Bahr and Graham Hutton. 2020. Calculating Correct Compilers II: Return of the Register Machines. Journal of Functional Programming (2020). To appear."},{"key":"e_1_3_2_1_5_1","volume-title":"LOLA 2018 - Syntax and Semantics of Low-Level Languages","author":"Barany Gerg\u00f6","year":"2018","unstructured":"Gerg\u00f6 Barany . 2018 . A more precise, more correct stack and register model for CompCert . In LOLA 2018 - Syntax and Semantics of Low-Level Languages 2018. Oxford, United Kingdom. https:\/\/hal.inria.fr\/hal-01799629 Gerg\u00f6 Barany. 2018. A more precise, more correct stack and register model for CompCert. In LOLA 2018 - Syntax and Semantics of Low-Level Languages 2018. Oxford, United Kingdom. https:\/\/hal.inria.fr\/hal-01799629"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1980.1653373"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1932681.1863585"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236950.3236965"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/3027670"},{"key":"e_1_3_2_1_11_1","unstructured":"Mitchell Pickard and Graham Hutton. 2020. Dependently-typed compilers don't go wrong. (2020). http:\/\/www.cs.nott.ac.uk\/~pszgmh\/well-typed.pdf In preparation.  Mitchell Pickard and Graham Hutton. 2020. Dependently-typed compilers don't go wrong. (2020). http:\/\/www.cs.nott.ac.uk\/~pszgmh\/well-typed.pdf In preparation."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/3077629.3077658"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133912"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022670.2951924"},{"key":"e_1_3_2_1_16_1","unstructured":"Agda Development Team. 2020. Agda. https:\/\/agda.readthedocs.io\/en\/latest\/  Agda Development Team. 2020. Agda. https:\/\/agda.readthedocs.io\/en\/latest\/"},{"key":"e_1_3_2_1_17_1","volume-title":"Implementation and Application of Functional Languages - 24th International Symposium, IFL","author":"van der Walt Paul","year":"2012","unstructured":"Paul van der Walt and Wouter Swierstra . 2012. Engineering Proof by Reflection in Agda . In Implementation and Application of Functional Languages - 24th International Symposium, IFL 2012 , Oxford, UK , August 30 - September 1, 2012, Revised Selected Papers (Lecture Notes in Computer Science), Ralf Hinze (Ed.), Vol. 8241 . Springer , 157--173. https:\/\/doi.org\/10.1007\/978-3-642-41582-1_10 10.1007\/978-3-642-41582-1_10 Paul van der Walt and Wouter Swierstra. 2012. Engineering Proof by Reflection in Agda. In Implementation and Application of Functional Languages - 24th International Symposium, IFL 2012, Oxford, UK, August 30 - September 1, 2012, Revised Selected Papers (Lecture Notes in Computer Science), Ralf Hinze (Ed.), Vol. 8241. Springer, 157--173. https:\/\/doi.org\/10.1007\/978-3-642-41582-1_10"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122975.3122979"}],"event":{"name":"SBLP '20: 24th Brazilian Symposium on Programming Languages","sponsor":["SBC Brazilian Computer Society"],"location":"Natal Brazil","acronym":"SBLP '20"},"container-title":["Proceedings of the 24th Brazilian Symposium on Context-Oriented Programming and Advanced Modularity"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3427081.3427086","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3427081.3427086","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:24Z","timestamp":1750197744000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3427081.3427086"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,19]]},"references-count":18,"alternative-id":["10.1145\/3427081.3427086","10.1145\/3427081"],"URL":"https:\/\/doi.org\/10.1145\/3427081.3427086","relation":{},"subject":[],"published":{"date-parts":[[2020,10,19]]},"assertion":[{"value":"2020-10-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}