{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/90544"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/90544","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Polarized substructural session types","abstract":"Concurrent processes can be extremely difficult to reason about, both for programmers and formally. One approach to coping with this difficulty is to study new programming languages and type features such as Session Types. Session types take as their conceptual notion of concurrency as a collection of processes linked together via channels and provide type-level coordination between processes using these channels. Logically motivated programming languages exploit the idea that providing a proof of a theorem in a logic is similar to proving that a given term has a particular type in a programming language and vice versa. These connections can be interesting for a few different reasons. First, when language and logic are independently discovered and independently useful, the existence of a connection suggests that both are onto some fundamentally important idea. Additionally, a connection provides a basis both for sanity checking our ideas and also can be fruitful grounds for inspiration by seeing how variants of either the logic or the language are reflected through the connection. This thesis primarily describes an exploration of logically motivated session types, SILL. Polarization, classifying propositions as either positive or negative, provides a natural way to describe a logically based session typing language with asynchronous communication while retaining a semantics that is reasonably implementable. Additionally, polarization gives us a way to smoothly integrate synchronous channels into SILL without needing a semantic extension. When combined with Adjoint Logic, this gives us an ability to incorporate a variety of modalities with relatively little work. From a practical perspective, this gives SILL access to persistent processes and garbage collection. We additionally explore a trio of loosely related extensions to SILL, and their logical connections, inspired by the above results: bundled message passing to reduce the number of communications performed by processes; racy programs, enabled by a select/epoll-like mechanism; and asynchronous receiving, an almost generalization of the basic asynchronous semantics. We have three different implementations of SILL: a simple but relatively full featured interpreter written in OCaml; a fragment of SILL as an embedded domain specific language in Haskell; and a cleaner version of the same in Idris. Lastly, we show that Liquid Types and Session Types are compatible. This gives us one notion of a dependently session typed language.","abstract_html":"Concurrent processes can be extremely difficult to reason about, both for programmers and formally. One approach to coping with this difficulty is to study new programming languages and type features such as Session Types. Session types take as their conceptual notion of concurrency as a collection of processes linked together via channels and provide type-level coordination between processes using these channels. Logically motivated programming languages exploit the idea that providing a proof of a theorem in a logic is similar to proving that a given term has a particular type in a programming language and vice versa. These connections can be interesting for a few different reasons. First, when language and logic are independently discovered and independently useful, the existence of a connection suggests that both are onto some fundamentally important idea. Additionally, a connection provides a basis both for sanity checking our ideas and also can be fruitful grounds for inspiration by seeing how variants of either the logic or the language are reflected through the connection. This thesis primarily describes an exploration of logically motivated session types, SILL. Polarization, classifying propositions as either positive or negative, provides a natural way to describe a logically based session typing language with asynchronous communication while retaining a semantics that is reasonably implementable. Additionally, polarization gives us a way to smoothly integrate synchronous channels into SILL without needing a semantic extension. When combined with Adjoint Logic, this gives us an ability to incorporate a variety of modalities with relatively little work. From a practical perspective, this gives SILL access to persistent processes and garbage collection. We additionally explore a trio of loosely related extensions to SILL, and their logical connections, inspired by the above results: bundled message passing to reduce the number of communications performed by processes; racy programs, enabled by a select/epoll-like mechanism; and asynchronous receiving, an almost generalization of the basic asynchronous semantics. We have three different implementations of SILL: a simple but relatively full featured interpreter written in OCaml; a fragment of SILL as an embedded domain specific language in Haskell; and a cleaner version of the same in Idris. Lastly, we show that Liquid Types and Session Types are compatible. This gives us one notion of a dependently session typed language.","abstract_has_math":false,"creators":["Griffith, Dennis Edward"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Gunter, Elsa L.","Pfenning, Frank","Gunter, Carl","Agha, Gul"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2016,"date_issued":"2016-07-07T19:53:56Z","date_published":"2016-07-07T19:53:56Z","updated_at":"2026-07-22T22:26:32Z","subjects":["Programming Languages","Session Types","Curry-Howard"],"languages":["en"],"rights":["Copyright 2016 Dennis Griffith"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/90544","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Gunter, Elsa L.","Pfenning, Frank","Gunter, Carl","Agha, Gul"]},{"key":"dc:creator","label":"Author","values":["Griffith, Dennis Edward"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2016-07-07T19:53:56Z","2016-04-20","2016-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":["Programming Languages","Session Types","Curry-Howard"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2016 Dennis Griffith"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/90544"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Concurrent processes can be extremely difficult to reason about, both for programmers and formally. One approach to coping with this difficulty is to study new programming languages and type features such as Session Types. Session types take as their conceptual notion of concurrency as a collection of processes linked together via channels and provide type-level coordination between processes using these channels. Logically motivated programming languages exploit the idea that providing a proof of a theorem in a logic is similar to proving that a given term has a particular type in a programming language and vice versa. These connections can be interesting for a few different reasons. First, when language and logic are independently discovered and independently useful, the existence of a connection suggests that both are onto some fundamentally important idea. Additionally, a connection provides a basis both for sanity checking our ideas and also can be fruitful grounds for inspiration by seeing how variants of either the logic or the language are reflected through the connection. This thesis primarily describes an exploration of logically motivated session types, SILL. Polarization, classifying propositions as either positive or negative, provides a natural way to describe a logically based session typing language with asynchronous communication while retaining a semantics that is reasonably implementable. Additionally, polarization gives us a way to smoothly integrate synchronous channels into SILL without needing a semantic extension. When combined with Adjoint Logic, this gives us an ability to incorporate a variety of modalities with relatively little work. From a practical perspective, this gives SILL access to persistent processes and garbage collection. We additionally explore a trio of loosely related extensions to SILL, and their logical connections, inspired by the above results: bundled message passing to reduce the number of communications performed by processes; racy programs, enabled by a select/epoll-like mechanism; and asynchronous receiving, an almost generalization of the basic asynchronous semantics. We have three different implementations of SILL: a simple but relatively full featured interpreter written in OCaml; a fragment of SILL as an embedded domain specific language in Haskell; and a cleaner version of the same in Idris. Lastly, we show that Liquid Types and Session Types are compatible. This gives us one notion of a dependently session typed language.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2016-07-07 without embargo terms","The student, Dennis Griffith, accepted the attached license on 2016-04-14 at 19:33.","The student, Dennis Griffith, submitted this Dissertation for approval on 2016-04-14 at 19:44.","This Dissertation was approved for publication on 2016-04-20 at 10:12.","DSpace SAF Submission Ingestion Package generated from Vireo submission #9233 on 2016-07-07 at 13:30:48","Made available in DSpace on 2016-07-07T19:53:56Z (GMT). No. of bitstreams: 7 GRIFFITH-DISSERTATION-2016.pdf: 1147900 bytes, checksum: 89901341df622d2a772ae3e898a80cd8 (MD5) haskell.tar.gz: 10942 bytes, checksum: 819b04d206620c7a60c6bcb7258a2540 (MD5) idris.tar.gz: 8560 bytes, checksum: 343dfda0372db78924da8b2b9608db02 (MD5) ocaml.tar.gz: 94418 bytes, checksum: 8f5ec2ccd94493b5c942633cf7930500 (MD5) thesis.tar.gz: 15166653 bytes, checksum: 7d54a830aa2990bf3951a598ef16e1d3 (MD5) LICENSE.txt: 4212 bytes, checksum: e4c4520089cf7930552cb83d8c16328a (MD5) PROQUEST_LICENSE.txt: 4558 bytes, checksum: acd03484828d23010a270ce15ce5eff9 (MD5) Previous issue date: 2016-04-20"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Polarized substructural session types"]}]}],"canonical_facts":{"dc:contributor":["Gunter, Elsa L.","Pfenning, Frank","Gunter, Carl","Agha, Gul"],"dc:creator":["Griffith, Dennis Edward"],"dc:date":["2016-07-07T19:53:56Z","2016-04-20","2016-05"],"dc:description":["Concurrent processes can be extremely difficult to reason about, both for programmers and formally. One approach to coping with this difficulty is to study new programming languages and type features such as Session Types. Session types take as their conceptual notion of concurrency as a collection of processes linked together via channels and provide type-level coordination between processes using these channels. Logically motivated programming languages exploit the idea that providing a proof of a theorem in a logic is similar to proving that a given term has a particular type in a programming language and vice versa. These connections can be interesting for a few different reasons. First, when language and logic are independently discovered and independently useful, the existence of a connection suggests that both are onto some fundamentally important idea. Additionally, a connection provides a basis both for sanity checking our ideas and also can be fruitful grounds for inspiration by seeing how variants of either the logic or the language are reflected through the connection. This thesis primarily describes an exploration of logically motivated session types, SILL. Polarization, classifying propositions as either positive or negative, provides a natural way to describe a logically based session typing language with asynchronous communication while retaining a semantics that is reasonably implementable. Additionally, polarization gives us a way to smoothly integrate synchronous channels into SILL without needing a semantic extension. When combined with Adjoint Logic, this gives us an ability to incorporate a variety of modalities with relatively little work. From a practical perspective, this gives SILL access to persistent processes and garbage collection. We additionally explore a trio of loosely related extensions to SILL, and their logical connections, inspired by the above results: bundled message passing to reduce the number of communications performed by processes; racy programs, enabled by a select/epoll-like mechanism; and asynchronous receiving, an almost generalization of the basic asynchronous semantics. We have three different implementations of SILL: a simple but relatively full featured interpreter written in OCaml; a fragment of SILL as an embedded domain specific language in Haskell; and a cleaner version of the same in Idris. Lastly, we show that Liquid Types and Session Types are compatible. This gives us one notion of a dependently session typed language.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2016-07-07 without embargo terms","The student, Dennis Griffith, accepted the attached license on 2016-04-14 at 19:33.","The student, Dennis Griffith, submitted this Dissertation for approval on 2016-04-14 at 19:44.","This Dissertation was approved for publication on 2016-04-20 at 10:12.","DSpace SAF Submission Ingestion Package generated from Vireo submission #9233 on 2016-07-07 at 13:30:48","Made available in DSpace on 2016-07-07T19:53:56Z (GMT). No. of bitstreams: 7 GRIFFITH-DISSERTATION-2016.pdf: 1147900 bytes, checksum: 89901341df622d2a772ae3e898a80cd8 (MD5) haskell.tar.gz: 10942 bytes, checksum: 819b04d206620c7a60c6bcb7258a2540 (MD5) idris.tar.gz: 8560 bytes, checksum: 343dfda0372db78924da8b2b9608db02 (MD5) ocaml.tar.gz: 94418 bytes, checksum: 8f5ec2ccd94493b5c942633cf7930500 (MD5) thesis.tar.gz: 15166653 bytes, checksum: 7d54a830aa2990bf3951a598ef16e1d3 (MD5) LICENSE.txt: 4212 bytes, checksum: e4c4520089cf7930552cb83d8c16328a (MD5) PROQUEST_LICENSE.txt: 4558 bytes, checksum: acd03484828d23010a270ce15ce5eff9 (MD5) Previous issue date: 2016-04-20"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/90544"],"dc:language":["en"],"dc:rights":["Copyright 2016 Dennis Griffith"],"dc:subject":["Programming Languages","Session Types","Curry-Howard"],"dc:title":["Polarized substructural session types"],"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:26:32Z"}