peps prose
In the domain of communication centric languages, the conception and reviewing process of a piece of research is slow and error prone due to the high level of formality that the subject requires. Interactive theorem provers proved to be a valuable tool for verifying the correctness of technical results in affine domains such as semantics of programming languages. Unfortunately, such tools are less used in concurrency theory because of the lack of domain-specific techniques and support libraries. We aim at filling this gap, in the typed mobile calculi area, so that the use of interactive theorem provers in the domain of session calculi becomes customary. With the help of this funding we aim at kicking off a network of collaborations between researchers interested to this topic.
year: 2019
