I am a fifth year PhD student at Carnegie Mellon University advised by Prof. Jan Hoffmann. I am broadly interested in programming languages with a specific focus on resource analysis, session types and language design for smart contracts on the blockchain.
I am the lead designer and developer of Nomos, a domain-specific language for implementing smart contracts. This language provides 4 key features, i) a session type based mechanism for expressing the contract protocol, ii) a resource type system for expressing and automatically verifying the gas bound of a transaction, iii) a linear type system to handle assets, and iv) a design guarantee of no re-entrancy attacks.
I have also designed Rast along with Prof. Frank Pfenning, a language implementing resource-aware session types with arithmetic refinements. This implementation complements my work on designing temporal and ergometric session types for parallel and sequential complexity analysis of concurrent session-typed programs.
Before joining CMU, I worked as a Research Fellow at Microsoft Research, India with Akash Lal where I developed an efficient method to perform precise alias analysis for C and C++ programs for Windows driver modules to automatically infer safe null pointer dereferences.
|Jul 2020||Our submission Exact and Linear-Time Gas-Cost Analysis has been accepted to SAS 2020.|
|Jul 2020||Finally, our submission Resource-Aware Session Types for Digital Contracts has been accepted to CSF 2021!|
|Jul 2020||Our submission Verified Linear Session-Typed Concurrent Programming has been accepted to PPDP 2020.|
|Jun 2020||Our submission Session Types with Arithmetic Refinements has been accepted to CONCUR 2020.|
|Jun 2020||Our paper Rast: Resource-Aware Session Types with Arithmetic Refinements has been awarded the best system decription paper by a junior researcher of FSCD 2020!|
|Apr 2020||Our latest submission Rast: Resource-Aware Session Types with Arithmetic Refinements has been accepted to FSCD 2020.|
|2019 — 2020||Invited talk titled Resource-Aware Session Types for Digital Contracts at Purdue University, University of Illinois, Urbana-Champaign, Facebook, Seattle, University of Washington, IIT Bombay, IIT Delhi and Microsoft Research, Bangalore.|
|Aug 2019||I just finished an amazing internship with Shaz Qadeer at Facebook. My goal was to design static gas analysis techniques for the Move language.|
|Feb 2019||I successfully proposed my thesis: Resource-Aware Session Types for Digital Contracts.|
Ishani is a second year BS student in the Computer Science department in Carnegie Mellon University.
Project: The base language of session types supports no functional programming or data structures, thus not practical for real-world programming. Nomos integrates session-based programming into a functional core using a linear contextual monad. Ishani was responsible for developing the theory and implementation for this integration. In a second project, Ishani has been adding subtyping to Nomos, again both in theory and implementation.
Stephen is a third year BS student in the Computer Science department in Carnegie Mellon University.
Project: Nomos is a general-purpose programming language integrating session types with functional programming with support for resource analysis. To support smart contract programming with Nomos, we need to also introduce blockchain-specific syntax and create blockchain-related data structures. Stephen is responsible for maintaining smart contracts in a session-type configuration to create the blockchain state, and the log of transactions to create the blockchain.