University of Illinois Urbana-Champaign

Polarized substructural session types

Griffith, Dennis Edward

Content Files
GRIFFITH-DISSERTATION-2016.pdf
haskell.tar.gz
idris.tar.gz
ocaml.tar.gz

Permalink

https://hdl.handle.net/2142/90544

Description

Title
Polarized substructural session types
Author(s)
Griffith, Dennis Edward
Issue Date
2016-04-20
Director of Research (if dissertation) or Advisor (if thesis)
Gunter, Elsa L.
Doctoral Committee Chair(s)
Gunter, Elsa L.
Committee Member(s)
  • Pfenning, Frank
  • Gunter, Carl
  • Agha, Gul
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Date of Ingest
2016-07-07T19:53:56Z
Keyword(s)
  • Programming Languages
  • Session Types
  • Curry-Howard
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.
Graduation Semester
2016-05
Type of Resource
text
Permalink
http://hdl.handle.net/2142/90544
Copyright and License Information
Copyright 2016 Dennis Griffith

Owning Collections

Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at Illinois