I am on the academic job market this cycle. Please reach out to me if you think I would be a good fit for your department. Below you can read my statements on research contributions, teaching philosophy, and diversity commitment.
I am a final year PhD student at Carnegie Mellon University advised by Prof. Jan Hoffmann, but also closely work with Prof. Frank Pfenning. 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.
|Dec 2020||Our submission Nested Session Types has been accepted to ESOP 2021.|
|Sep 2020||Super excited to release the web interface for the Nomos language. You can now use our implementation to check and execute transactions, as well as infer their gas bounds automatically!|
|2019 — 2020||Invited talk titled Resource-Aware Session Types for Digital Contracts at Stanford University; Harvard University; Imperial College, London; University of Edinburgh; University of Colorado, Boulder; Massachusetts Institute of Technology; New York University; Princeton Univeristy; University of California, San Diego; University of Texas, Austin; University of Wisconsin, Madison; Cornell University; Boston University; Yale University; University of Illinois, Urbana-Champaign; Facebook, Seattle; University of Washington; IIT Bombay; IIT Delhi; and Microsoft Research, Bangalore.|
|Jul 2020||Our submission Exact and Linear-Time Gas-Cost Analysis has been accepted to SAS 2020. This paper was the result of an amazing internship with Shaz Qadeer at Facebook in summer 2019.|
|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!|
|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.