Sessionstyper modell strukturerad kommunikation-baserad programmering. Framför allt beskriver binära sessionstyper för π-calculus kommunikation mellan exakt två deltagare i ett distribuerat scenario. Att lägga till sessioner i π-calculus innebär att utöka det med typ- och termkonstruktioner. I ett tidigare dokument försökte vi förstå i vilken utsträckning sessionskonstruktionerna är mer komplexa och uttrycksfulla än standard π-kalculus-konstruktionerna. Således presenterade vi en kodning av binär session π-calculus till standardtyped π-calculus genom att anta linjära och varianttyper och fortsättning-passing princip. I detta dokument fokuserar vi på rekursiva sessionstyper och presenterar en kodning till rekursiva linjära π-typer. Denna kodning är en konservativ förlängning av den förra genom att den bevarar de resultat som erhålls däri. Viktigast av allt, antar det en ny behandling av dualitetsförhållandet, som i närvaro av rekursiva typer har visat sig vara ganska utmanande.
Dardha REF ger en kodning av rekursiva sessions-typade π-kalculus till rekursiva (icke-linjära) π-kalculus, och visar att denna kodning bevarar både maskinskrivning och semantik.
Recursive Session Types Revisited
{'venue': 'EPTCS 162, 2014, pp. 27-34', 'journal': None, 'mag_field_of_study': ['Computer Science']}