Tianyu Chen

Welcome to Tianyu's Home Page!

Profile picture:

Research Interests

I am a PhD candidate in Computer Science at Indiana University Bloomington, advised by Professor Jeremy G. Siek. I am a member of PL wonks.

I enjoy building mechanized proofs and formalizing programming languages in proof assistants. My recent work focuses on reasoning about gradually typed languages, where some of the type information is statically unknown, and modeling their properties in Agda.

I am the lead associate instructor for CSCI C343 Data Structures in Spring 2024.

I organized the Programming Languages Reading Group (PLRG) from 2021 to 2023.

I was a software verification intern at CertiK during summer 2021, where I worked on certifying the functional correctness of system software using Coq and CompCert.

Recent Projects

Gradual Security Typing link
Parameterized Cast Calculi link


  • Quest Complete: the Holy Grail of Gradual Security NEW!
    Tianyu Chen, Jeremy G. Siek
    Arxiv PDF PL Wonks
  • Mechanized Noninterference for Gradual Security
    Tianyu Chen, Jeremy G. Siek
    Arxiv PDF Code

Refereed Articles

  • Parameterized Cast Calculi and Reusable Meta-theory for Gradually Typed Lambda Calculi
    Jeremy G. Siek, Tianyu Chen
    Journal of Functional Programming
    DOI Arxiv Code
  • Mechanized Type Safety for Gradual Information Flow
    Tianyu Chen, Jeremy G. Siek
    LangSec 2021
    DOI PDF Talk Slides Code
  • Racing in Hyperspace: Closing Hyper-threading Side Channels on SGX with Contrived Data Races
    Guoxing Chen, Wenhao Wang, Tianyu Chen, Sanchuan Chen, Yinqian Zhang, XiaoFeng Wang, Ten-Hwang Lai, Dongdai Lin
    IEEE Security and Privacy 2018
  • Characterizing Smartwatch Usage in the Wild
    Xing Liu, Tianyu Chen, Feng Qian, Zhixiu Guo, Felix Xiaozhu Lin, Xiaofeng Wang, Kai Chen
    MobiSys 2017
  • Paxos Made Transparent
    Heming Cui, Rui Gu, Cheng Liu, Tianyu Chen, Junfeng Yang
    SOSP 2015

Posters & Extended Abstracts


Associate Instructor Data Structures CSCI-C343 Spring 2024
Associate Instructor Data Structures, Honors CSCI-H343 Fall 2023
Associate Instructor Secure Protocols CSCI-B433, INFO-I433 Spring 2020
Associate Instructor Malware: Threat and Defense CSCI-B546, INFO-I521 Fall 2019
Associate Instructor Secure Protocols CSCI-B433, INFO-I433 Spring 2019


  • Indiana University academic calendar link
  • Spacemacs Agda layer link

Contact Information

  • Email: \(\mathtt{chen512} @ \mathtt{indiana} . \mathtt{edu}\)
  • Office: Cubicle 3025B. Luddy Hall, Indiana University. 700 N. Woodlawn Ave. Bloomington, IN 47408

Created: 2024-01-24 Wed 13:25