Computer Sciences and Information Technology
Title : | Session Types Applications, Foundations and Flow Security (STAFFS) |
Area of research : | Computer Sciences and Information Technology |
Focus area : | Programming Languages |
Principal Investigator : | Prof. Sanjiva Prasad, Indian Institute of Technology (IIT), New Delhi (110016) |
Contact info : | sanjiva@cse.iitd.ac.in;
sak@cse.iitd.ac.in |
Details
Executive Summary : | 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. |
Co-PI: | Prof. S Arun Kumar, Indian Institute of Technology (IIT), New Delhi (110016) |
Total Budget (INR): | 12,15,000 |
Organizations involved