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.

**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'm part of PL Wonks at IU, and I helped run the Type Theory Reading Group.

I was a Research Assistant in the IU Parfunc group led by Ryan Newton.

I have been a Google Summer of Code participant, as a student and a mentor for the Gentoo Foundation.

I'm involved with Navya, HackCave and the IITK-NYC Office.

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
USA
```