Google Scholar
ankushd [AT] cs . cmu . edu
Github
Bitbucket
ResearchGate
9225 Gates and Hillman
Centers, CMU
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.
I completed my undergraduate at IIT Bombay, India in 2015 where I worked with Prof. Supratik Chakraborty and Prof. Akshay S on deciding termination of linear loop programs.
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. |
Ankush Das, Henry DeYoung, Andreia Mordido and Frank Pfenning.
In Proceedings of the 30th European Symposium on Programming.
Ankush Das, Di Wang and Jan Hoffmann.
Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning and Ishani Santurkar.
In Proceedings of the 34th IEEE Computer Security Foundations Symposium.
Ankush Das and Shaz Qadeer.
In Proceedings of the 27th International Static Analysis Symposium.
Ankush Das and Frank Pfenning.
In Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming.
Ankush Das and Frank Pfenning.
In Proceedings of the 31st International Conference on Concurrency Theory.
Ankush Das and Frank Pfenning.
In Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction.
Best system decription paper award by a junior researcher
Ankush Das and Frank Pfenning.
Ankush Das, Jan Hoffmann and Frank Pfenning.
In 23rd International Conference on Functional Programming.
Ankush Das, Jan Hoffmann and Frank Pfenning.
In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science.
S. Akshay, Supratik Chakraborty, Ankush Das, Vishal Jagannath and Sai Sandeep.
In Proceedings of the 28th International Conference on Concurrency Theory.
Ankush Das and Akash Lal.
In Proceedings of the 15th International Symposium on Automated Technology for Verification and Analysis.
Ankush Das and Jan Hoffmann.
In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems.
Jan Hoffmann, Ankush Das and Shu-Chun Weng.
In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages.
Ankush Das and Jan Hoffmann.
Workshop on Syntax and Semantics of Low-Level Languages
Ankush Das, Shuvendu K. Lahiri, Akash Lal, Yi Li.
In Proceedings of the 27th International Conference on Computer Aided Verification.
Ankush Das, Shankara Narayanan Krishna, Lakshmi Manasa, Ashutosh Trivedi, Dominik Wojtczak.
In Proceedings of the 12th Annual Conference on Theory and Applications of Models of Computation.
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.
CS 15-814, Carnegie Mellon University, Fall 2016.
Instructor: Karl Crary
CS 15-317, Carnegie Mellon University, Fall 2018.
Instructor: Karl Crary