I am a doctoral candidate at Indiana University Bloomington, advised by Amr Sabry. I'm currently a visiting researcher at the Computer Laboratory, University of Cambridge, working with Marcelo Fiore and Neel Krishnaswami.


I study type theories and programming languages, through the lens of category theory. I'm also interested in mathematical logic, constructive mathematics, and formalization.


My papers are listed on arXiv and dblp.

  • Vikraman Choudhury, Neel Krishnaswami: Recovering Purity with Comonads and Capabilities. To appear in ICFP 2020.
  • Chao-Hong Chen, Vikraman Choudhury, Jacques Carette, Amr Sabry: Fractional Types: Expressive and Safe Space Management for Ancilla Bits. To appear in RC 2020.
  • Jacques Carette, Chao-Hong Chen, Vikraman Choudhury, Amr Sabry: From Reversible Programs to Univalent Universes and Back. MFPS XIII, ENTCS 336, 2018.
  • Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, Ranjit Jhala: Refinement reflection: complete verification with SMT. POPL 2018.
  • Chao-Hong Chen, Vikraman Choudhury, Ryan R. Newton: Adaptive lock-free data structures in Haskell: a general method for concurrent implementation swapping. Haskell 2017.


  • Ryan G. Scott, Vikraman Choudhury, Ryan R. Newton, Niki Vazou, Ranjit Jhala: Deriving Law-Abiding Instances. 2017.
  • Jacques Carette, Chao-Hong Chen, Vikraman Choudhury, Amr Sabry: Fractional Types. 2016.

Selected Talks

  • Recovering Purity with Comonads & Capabilities. Midwest PL Summit 2019, Purdue University. Sep 2019.
  • The finite-multiset construction in HoTT. HoTT 2019, CMU. Aug 2019.
  • Retrofitting Purity with Comonads & Capabilities. Logic and Semantics Seminar, CL, Cambridge. May 2019.
  • Beth Semantics. Proof Theory and Constructive Mathematics Seminar, IU. Dec 2018.

  • Automorphisms of ๐•Šยน. PL Wonks, IU. Oct 2018.

  • Homotopy theoretic aspects of Reversible Computing. PL Wonks, IU. Sep 2017.


  • Distributed Issue Tracking using Patch Theory. Masters Thesis, IIT Kanpur, 2015.



At Cambridge, I supervise

  • Discrete Maths
  • Semantics of Programming Languages
  • Denotational Semantics
  • Logic and Proof

At IU, I've taught

  • B-561: Advanced Database Concepts
  • B-401: Fundamentals of Computing Theory
  • B-505: Applied Algorithms
  • I-590: Technical Foundations of Cybersecurity
  • C-343: Data Structures
  • C-241 & H-241: Discrete Structures for Computer Science
  • C-211: Intro to Computer Science



I can be reached via email (alternative), or irc ([email protected]freenode), or smail at the following address:

Luddy Hall, 3025Q
700 N. Woodlawn Avenue
Bloomington, IN 47408