Vi föreslår ett typsystem för låsfrihet i π-kalculus, som garanterar att vissa kommunikationer så småningom kommer att lyckas. Särskiljande funktioner hos vårt typsystem är: det kan verifiera låsfrihet för samtidiga program som har sofistikerade rekursiva kommunikationsstrukturer; det kan vara helt automatiserad; det är hybrid, genom att det kombinerar ett typsystem för låsfrihet med lokala resonemang om dödlägesfrihet, uppsägning och konfluensanalyser. Dessutom är typsystemet parameteriserat med dödlägesfrihet/avslutande/konfluensanalyser, så att alla metoder (t.ex. Typsystem och modellkontroll) kan användas för dessa analyser. Ett verktyg för låsfrihetsanalys har implementerats baserat på det föreslagna typsystemet och testats för icke-triviala program.
Kobayashi och Sangiorgi REF föreslår ett typsystem som bevisar låsfrihet för program skrivna i π-kalculus.
A hybrid type system for lock-freedom of mobile processes
{'venue': 'TOPL', 'journal': None, 'mag_field_of_study': ['Computer Science']}