{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/108050"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/108050","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Closing the gap in the LLVM backend of K","abstract":"In this thesis, we further develop part of the K framework, a framework for specifying and executing the formal semantics of languages. We dive into the LLVM backend, one of the engines for concrete execution, and implement key functionality that is present in the other concrete execution engine. We then add a new interface that is unique to the LLVM backend, making this backend diverge from the other backend. Finally, with the backend caught up and divergent, we implement and evaluate pattern matching optimization strategies.","abstract_html":"In this thesis, we further develop part of the K framework, a framework for specifying and executing the formal semantics of languages. We dive into the LLVM backend, one of the engines for concrete execution, and implement key functionality that is present in the other concrete execution engine. We then add a new interface that is unique to the LLVM backend, making this backend diverge from the other backend. Finally, with the backend caught up and divergent, we implement and evaluate pattern matching optimization strategies.","abstract_has_math":false,"creators":["Abir, Michael"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Rosu, Grigore"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2020,"date_issued":"2020-08-26T21:58:05Z","date_published":"2020-08-26T21:58:05Z","updated_at":"2026-07-22T22:24:47Z","subjects":["programming languages, rewriting-based execution, optimization"],"languages":["en"],"rights":["Copyright 2020 Michael Abir"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/108050","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Rosu, Grigore"]},{"key":"dc:creator","label":"Author","values":["Abir, Michael"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2020-08-26T21:58:05Z","2020-05-14","2020-05"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["programming languages, rewriting-based execution, optimization"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2020 Michael Abir"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/108050"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["In this thesis, we further develop part of the K framework, a framework for specifying and executing the formal semantics of languages. We dive into the LLVM backend, one of the engines for concrete execution, and implement key functionality that is present in the other concrete execution engine. We then add a new interface that is unique to the LLVM backend, making this backend diverge from the other backend. Finally, with the backend caught up and divergent, we implement and evaluate pattern matching optimization strategies.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2020-08-25 without embargo terms","The student, Michael Abir, accepted the attached license on 2020-05-12 at 15:03.","The student, Michael Abir, submitted this Thesis for approval on 2020-05-12 at 17:22.","This Thesis was approved for publication on 2020-05-14 at 10:49.","DSpace SAF Submission Ingestion Package generated from Vireo submission #15363 on 2020-08-25 at 17:14:23","Made available in DSpace on 2020-08-26T21:58:05Z (GMT). No. of bitstreams: 2 ABIR-THESIS-2020.pdf: 697435 bytes, checksum: 9bcdc746acd0405efe9fc204454ccbe4 (MD5) LICENSE.txt: 4209 bytes, checksum: 21ac68bd71b0e83081a7b2ee769f9dbb (MD5) Previous issue date: 2020-05-14"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Closing the gap in the LLVM backend of K"]}]}],"canonical_facts":{"dc:contributor":["Rosu, Grigore"],"dc:creator":["Abir, Michael"],"dc:date":["2020-08-26T21:58:05Z","2020-05-14","2020-05"],"dc:description":["In this thesis, we further develop part of the K framework, a framework for specifying and executing the formal semantics of languages. We dive into the LLVM backend, one of the engines for concrete execution, and implement key functionality that is present in the other concrete execution engine. We then add a new interface that is unique to the LLVM backend, making this backend diverge from the other backend. Finally, with the backend caught up and divergent, we implement and evaluate pattern matching optimization strategies.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2020-08-25 without embargo terms","The student, Michael Abir, accepted the attached license on 2020-05-12 at 15:03.","The student, Michael Abir, submitted this Thesis for approval on 2020-05-12 at 17:22.","This Thesis was approved for publication on 2020-05-14 at 10:49.","DSpace SAF Submission Ingestion Package generated from Vireo submission #15363 on 2020-08-25 at 17:14:23","Made available in DSpace on 2020-08-26T21:58:05Z (GMT). No. of bitstreams: 2 ABIR-THESIS-2020.pdf: 697435 bytes, checksum: 9bcdc746acd0405efe9fc204454ccbe4 (MD5) LICENSE.txt: 4209 bytes, checksum: 21ac68bd71b0e83081a7b2ee769f9dbb (MD5) Previous issue date: 2020-05-14"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/108050"],"dc:language":["en"],"dc:rights":["Copyright 2020 Michael Abir"],"dc:subject":["programming languages, rewriting-based execution, optimization"],"dc:title":["Closing the gap in the LLVM backend of K"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:47Z"}