Executive Summary : | The project aims to explore the logical connections between security properties, control constructs, and type systems. It will explore secure session types and their applications to multiparty interactions, develop analysis techniques and software tools, and establish long-term research connections between IITD and the Mathematical Institute of the Serbian Academy of Science and Arts and U. Novi Sad. The primary deliverables include research papers, software analysis tools, and verification environments for type-based analyses. Distributed communicating software systems are designed to work correctly and securely by ensuring each component adheres to the desired protocol. Session types are a successful solution to this problem, providing a type-based methodology to verify if a given process correctly implements a desired protocol. They have been implemented in mainstream programming languages like Java, Python, Go, Scala, C, TypeScript, F, OCaml, Haskell, and Erlang. Session type systems are based on the Curry-Howard C-H Correspondence, which connects proof theoretical accounts of logic with computation theory. |