중첩 세션 타입을 이용한 비동기 프로세스의 표현력에 대하여

요약

본 논문은 전통적인 세션 타입의 한계를 극복하는 중첩 세션 타입(NST)을 다룹니다. NST를 활용한 비동기 세션 프로세스(ASP)가 2카운터 기계 인코딩을 통해 유형화된 프로세스로 구현 가능함을 증명했습니다. 이를 통해 ASP는 강력한 표현력을 가지며 튜링 완전성을 가짐을 입증하였습니다.

핵심 포인트

• 전통적 세션 타입은 정규 프로토콜만 표현 가능하다는 한계가 있습니다.
• 중첩 세션 타입(NST)은 중첩된 재귀적 프로토콜 지정이 가능합니다.
• 비동기 세션 프로세스(ASP)의 표현력을 연구했습니다.
• ASP는 2카운터 기계를 인코딩하여 튜링 완전함을 증명했습니다.