System $F^\mu_\omega$ with Context-free Session Types
| Autor: | Costa, Diana, Mordido, Andreia, Poças, Diogo, Vasconcelos, Vasco T. |
|---|---|
| Rok vydání: | 2023 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | We study increasingly expressive type systems, from $F^\mu$ -- an extension of the polymorphic lambda calculus with equirecursive types -- to $F^{\mu;}_\omega$ -- the higher-order polymorphic lambda calculus with equirecursive types and context-free session types. Type equivalence is given by a standard bisimulation defined over a novel labelled transition system for types. Our system subsumes the contractive fragment of $F^\mu_\omega$ as studied in the literature. Decidability results for type equivalence of the various type languages are obtained from the translation of types into objects of an appropriate computational model: finite-state automata, simple grammars and deterministic pushdown automata. We show that type equivalence is decidable for a significant fragment of the type language. We further propose a message-passing, concurrent functional language equipped with the expressive type language and show that it enjoys preservation and absence of runtime errors for typable processes. Comment: 38 pages, 13 figures |
| Databáze: | arXiv |
| Externí odkaz: |
|