Gradual session types

摘要: Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims come with systems to communications. However, web-based applications and microservices often written in mix languages, disciplines spectrum between static dynamic typing. Gradual session address this mixed setting by providing framework which grants seamless transition statically typed handling sessions any required degree We propose GV as gradually extension functional system GV. Following standard gradual typing, consists an external language, relaxes using types; internal language casts, for operational semantics is given; cast-insertion translation from former latter. demonstrate communication well blame safety, thus extending previous results languages session-based communication. The interplay linearity requires novel approach specifying dynamics language.