Abstrakt. Vi presenterar en rekonstruktion av sessionstyper i en konventionell pi-kalkyl där typer är kvalificerade som linjära eller obegränsade. Linjärt inskrivna kommunikationskanaler är garanterade att förekomma i exakt en tråd, eventuellt flera gånger. Vi utrustar typer med en konstruktör som betecknar de två ändarna av en och samma kommunikationskanal. För att bedöma flexibiliteten i det nya typsystemet tillhandahåller vi tre distinkta kodningar (från den linjära lambdakalkylen, från den linjära pi-kalkylen, och från pi-kalkylen med polariserade variabler) in i vårt system. För varje språk presenterar vi operativa och skriva korrespondenser, visar att vårt system effektivt subsumerar den linjära pi-kalkylen samt föregående verk på sessionstyper.
Giunti och Vasconcelos REF ger ett typsystem för π-kalculus med typbevarande teorem.
A linear account of session types in the pi calculus
{'venue': 'CONCUR', 'journal': None, 'mag_field_of_study': ['Computer Science']}