We introduce Regular Session Types (RST), a (binary, synchronous, classical) session-typed calculus for which we prove a direct correspondence with regular languages, in addition to progress and preservation. Compared to recent studies of regularity in session types, RST’s contribution is that it makes the treatment of regularity particularly straightforward. To achieve this, the main technical novelties in RST are the internalization of iteration as a first-class type connective and the stratification of session types into read and write session types. The read and write types correspond directly to negative and positive types from polarized session types with one key modification: positive and negative operators are not freely intermixed.

Creator

• Friedman, Alex

Colaboradores

• Bohrer, Rose
• Heineman, George

Degree

• MS

Unit

• Computer Science

Publisher

• Worcester Polytechnic Institute

Identifier

• etd-114547

Palavra-chave

• Exponential Types
• Regular Languages
• RST
• Session Types
• Program Synthesis

Advisor

• Bohrer, Rose

Orcid

• https://orcid.org/0009-0000-6367-7885

Defense date

• 2023-11-28

Year

• 2023

Date created

• 2023-11-16

Resource type

• Thesis

Source

• etd-114547

Rights statement

• In Copyright

Última modificação

• 2024-01-25