Research Projects

Session types are essential for distributed communicating systems to prevent deadlocks and unmatched communication events. They are rooted in logic, proof theory, and programming, with propositions related to types, proofs to programs, and proof normalisation to program execution. The project aims to explore the logical connections between security properties, control constructs, and type systems, as well as secure session types and their applications to multiparty interactions. The project will develop analysis techniques and software tools for secure and safe multiparty interactive systems, establishing long-term research connections between IITD and the Mathematical Institute of the Serbian Academy of Science and Arts. 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.