{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/117836"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/117836","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Types for mutual exclusion in concurrent programming languages","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-04-12 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-04-12 without embargo terms","abstract_has_math":false,"creators":["Lee, John J"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Gunter, Elsa L"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2022,"date_issued":"2022-12","date_published":"2022-12","updated_at":"2026-07-22T22:24:56Z","subjects":["Formal Verification","Type Systems","Concurrent Programming"],"languages":["en","eng"],"rights":["Copyright 2022 John J. Lee"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/117836","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Gunter, Elsa L"]},{"key":"dc:creator","label":"Author","values":["Lee, John J"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2022-12","2022-12-06"]},{"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":["Formal Verification","Type Systems","Concurrent Programming"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en","eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2022 John J. Lee"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/117836"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-04-12 without embargo terms","The student, John Lee, accepted the attached license on 2022-12-05 at 22:15.","The student, John Lee, submitted this Thesis for approval on 2022-12-05 at 22:20.","This Thesis was approved for publication on 2022-12-06 at 09:42.","DSpace SAF Submission Ingestion Package generated from Vireo submission #18756 on 2023-04-12 at 07:38:49","One of the most difficult parts of writing concurrent programs is working with shared memory. It is difficult to reason about sections of code working on shared memory because of the possibility of interference from other threads of execution. This interference can be prevented by enforcing the mutual exclusion of resources, but guaranteeing this property is itself a difficult problem. One common way of statically enforcing mutual exclusion is through the use of linear type systems. Linear type systems impose a requirement that values designated as \"linear\" are used exactly once. This property is useful for several memory safety problems, including the enforcement of mutual exclusion of resources. However, linear type systems used in imperative code require a linearization on the order of imperative operations, rewriting code into a declarative style. In practice, this is inconvenient for programs that makes heavy use of mutable data structures. In order to maintain mutual exclusion of memory in an imperative language, rather than having a type system that requires resources to be single-use, we propose a type system that enforces \"single-ownership\" of resources, that at any given point in time, a resource is only owned by one thread of execution. The goal of this type system is to obtain mutual exclusion (or race-freedom) for a concurrent language that does not require a linearization of imperative operations. In this thesis, we present a novel type system that can perform this memory analysis for an imperative, higher-order, concurrent language. We state and prove results about the safety and soundness of our type system, and we also present an inference algorithm that can be used to check whether an arbitrary program is typable."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Types for mutual exclusion in concurrent programming languages"]}]}],"canonical_facts":{"dc:contributor":["Gunter, Elsa L"],"dc:creator":["Lee, John J"],"dc:date":["2022-12","2022-12-06"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-04-12 without embargo terms","The student, John Lee, accepted the attached license on 2022-12-05 at 22:15.","The student, John Lee, submitted this Thesis for approval on 2022-12-05 at 22:20.","This Thesis was approved for publication on 2022-12-06 at 09:42.","DSpace SAF Submission Ingestion Package generated from Vireo submission #18756 on 2023-04-12 at 07:38:49","One of the most difficult parts of writing concurrent programs is working with shared memory. It is difficult to reason about sections of code working on shared memory because of the possibility of interference from other threads of execution. This interference can be prevented by enforcing the mutual exclusion of resources, but guaranteeing this property is itself a difficult problem. One common way of statically enforcing mutual exclusion is through the use of linear type systems. Linear type systems impose a requirement that values designated as \"linear\" are used exactly once. This property is useful for several memory safety problems, including the enforcement of mutual exclusion of resources. However, linear type systems used in imperative code require a linearization on the order of imperative operations, rewriting code into a declarative style. In practice, this is inconvenient for programs that makes heavy use of mutable data structures. In order to maintain mutual exclusion of memory in an imperative language, rather than having a type system that requires resources to be single-use, we propose a type system that enforces \"single-ownership\" of resources, that at any given point in time, a resource is only owned by one thread of execution. The goal of this type system is to obtain mutual exclusion (or race-freedom) for a concurrent language that does not require a linearization of imperative operations. In this thesis, we present a novel type system that can perform this memory analysis for an imperative, higher-order, concurrent language. We state and prove results about the safety and soundness of our type system, and we also present an inference algorithm that can be used to check whether an arbitrary program is typable."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/117836"],"dc:language":["en","eng"],"dc:rights":["Copyright 2022 John J. Lee"],"dc:subject":["Formal Verification","Type Systems","Concurrent Programming"],"dc:title":["Types for mutual exclusion in concurrent programming languages"],"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:56Z"}