{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/101036"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/101036","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Actor programming with static guarantees","abstract":"Made available in DSpace on 2018-09-04T20:27:21Z (GMT). No. of bitstreams: 3 CHARALAMBIDES-DISSERTATION-2018.pdf: 1124015 bytes, checksum: 46e2c9f8cd78a18c8d49c5fb30d10c36 (MD5) LICENSE.txt: 4216 bytes, checksum: a917fbeb4b25cf6f0907c6c623345d95 (MD5) PROQUEST_LICENSE.txt: 4562 bytes, checksum: b80b97f53772c11c6ede41b07910e5cd (MD5) Previous issue date: 2018-04-20","abstract_html":"Made available in DSpace on 2018-09-04T20:27:21Z (GMT). No. of bitstreams: 3 CHARALAMBIDES-DISSERTATION-2018.pdf: 1124015 bytes, checksum: 46e2c9f8cd78a18c8d49c5fb30d10c36 (MD5) LICENSE.txt: 4216 bytes, checksum: a917fbeb4b25cf6f0907c6c623345d95 (MD5) PROQUEST_LICENSE.txt: 4562 bytes, checksum: b80b97f53772c11c6ede41b07910e5cd (MD5) Previous issue date: 2018-04-20","abstract_has_math":false,"creators":["Charalambides, Minas"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Agha, Gul A.","Parthasarathy, Madhusudan","Gunter, Elsa L.","Ravara, Antonio"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2018,"date_issued":"2018-09-04T20:27:21Z","date_published":"2018-09-04T20:27:21Z","updated_at":"2026-07-22T22:24:38Z","subjects":["actors","type","static","session","concurrency"],"languages":["en"],"rights":["Copyright 2018 Minas Charalambides"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/101036","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Agha, Gul A.","Parthasarathy, Madhusudan","Gunter, Elsa L.","Ravara, Antonio"]},{"key":"dc:creator","label":"Author","values":["Charalambides, Minas"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2018-09-04T20:27:21Z","2018-04-20","2018-05"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"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":["actors","type","static","session","concurrency"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2018 Minas Charalambides"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/101036"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Made available in DSpace on 2018-09-04T20:27:21Z (GMT). No. of bitstreams: 3 CHARALAMBIDES-DISSERTATION-2018.pdf: 1124015 bytes, checksum: 46e2c9f8cd78a18c8d49c5fb30d10c36 (MD5) LICENSE.txt: 4216 bytes, checksum: a917fbeb4b25cf6f0907c6c623345d95 (MD5) PROQUEST_LICENSE.txt: 4562 bytes, checksum: b80b97f53772c11c6ede41b07910e5cd (MD5) Previous issue date: 2018-04-20","This thesis discusses two methodologies for applying type discipline to concurrent programming with actors: process types, and session types. A system based on each of the two is developed, and used as the basis for a comprehensive overview of process- and session- type merits and limitations. In particular, we analyze the trade-offs of the two approaches with regard to the expressiveness of the resulting calculi, versus the nature of the static guarantees offered. The first system discussed is based on the notion of a \\emph{typestate}, that is, a view of an actor's internal state that can be statically tracked. The typestates used here capture what each actor handle \\emph{may} be used for, as well as what it \\emph{must} be used for. This is done by associating two kinds of tokens with each actor handle: tokens of the first kind are consumed when the actor receives a message, and thus dictate the types of messages that can be sent through the handle; tokens of the second kind dictate messaging obligations, and the type system ensures that related messages have been sent through the handle by the end of its lifetime. The next system developed here adapts session types to suit actor programming. Session types come from the world of process calculi, and are a means to statically check the messaging taking place over communication channels against a pre-defined protocol. Since actors do not use channels, one needs to consider pairs of actors as participants in multiple, concurrently executed---and thus interleaving---protocols. The result is a system with novel, parameterized type constructs to capture communication patterns that prior work cannot handle, such as the sliding window protocol. Although this system can statically verify the implementation of complicated messaging patterns, it requires deviations from industry-standard programming models---a problem that is true for all session type systems in the literature. This work argues that the typestate-based system, while not enforcing protocol fidelity as the session-inspired one does, is nevertheless more suitable for model actor calculi adopted by practical, already established frameworks such as Erlang and Akka.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2018-08-31 without embargo terms","The student, Minas Charalambides, accepted the attached license on 2018-04-20 at 12:44.","The student, Minas Charalambides, submitted this Dissertation for approval on 2018-04-20 at 13:19.","This Dissertation was approved for publication on 2018-04-20 at 17:23.","DSpace SAF Submission Ingestion Package generated from Vireo submission #12404 on 2018-08-31 at 17:14:01"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Actor programming with static guarantees"]}]}],"canonical_facts":{"dc:contributor":["Agha, Gul A.","Parthasarathy, Madhusudan","Gunter, Elsa L.","Ravara, Antonio"],"dc:creator":["Charalambides, Minas"],"dc:date":["2018-09-04T20:27:21Z","2018-04-20","2018-05"],"dc:description":["Made available in DSpace on 2018-09-04T20:27:21Z (GMT). No. of bitstreams: 3 CHARALAMBIDES-DISSERTATION-2018.pdf: 1124015 bytes, checksum: 46e2c9f8cd78a18c8d49c5fb30d10c36 (MD5) LICENSE.txt: 4216 bytes, checksum: a917fbeb4b25cf6f0907c6c623345d95 (MD5) PROQUEST_LICENSE.txt: 4562 bytes, checksum: b80b97f53772c11c6ede41b07910e5cd (MD5) Previous issue date: 2018-04-20","This thesis discusses two methodologies for applying type discipline to concurrent programming with actors: process types, and session types. A system based on each of the two is developed, and used as the basis for a comprehensive overview of process- and session- type merits and limitations. In particular, we analyze the trade-offs of the two approaches with regard to the expressiveness of the resulting calculi, versus the nature of the static guarantees offered. The first system discussed is based on the notion of a \\emph{typestate}, that is, a view of an actor's internal state that can be statically tracked. The typestates used here capture what each actor handle \\emph{may} be used for, as well as what it \\emph{must} be used for. This is done by associating two kinds of tokens with each actor handle: tokens of the first kind are consumed when the actor receives a message, and thus dictate the types of messages that can be sent through the handle; tokens of the second kind dictate messaging obligations, and the type system ensures that related messages have been sent through the handle by the end of its lifetime. The next system developed here adapts session types to suit actor programming. Session types come from the world of process calculi, and are a means to statically check the messaging taking place over communication channels against a pre-defined protocol. Since actors do not use channels, one needs to consider pairs of actors as participants in multiple, concurrently executed---and thus interleaving---protocols. The result is a system with novel, parameterized type constructs to capture communication patterns that prior work cannot handle, such as the sliding window protocol. Although this system can statically verify the implementation of complicated messaging patterns, it requires deviations from industry-standard programming models---a problem that is true for all session type systems in the literature. This work argues that the typestate-based system, while not enforcing protocol fidelity as the session-inspired one does, is nevertheless more suitable for model actor calculi adopted by practical, already established frameworks such as Erlang and Akka.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2018-08-31 without embargo terms","The student, Minas Charalambides, accepted the attached license on 2018-04-20 at 12:44.","The student, Minas Charalambides, submitted this Dissertation for approval on 2018-04-20 at 13:19.","This Dissertation was approved for publication on 2018-04-20 at 17:23.","DSpace SAF Submission Ingestion Package generated from Vireo submission #12404 on 2018-08-31 at 17:14:01"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/101036"],"dc:language":["en"],"dc:rights":["Copyright 2018 Minas Charalambides"],"dc:subject":["actors","type","static","session","concurrency"],"dc:title":["Actor programming with static guarantees"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:38Z"}