Tianyu Chen

Welcome to Tianyu's Home Page!

Profile picture:

Contact Information

  • Email: \(\mathtt{chen512} @ \mathtt{iu} . \mathtt{edu}\)
  • Office: 3025B. Luddy Hall, Indiana University. 700 N. Woodlawn Ave. Bloomington, IN 47408
  • ORCID: 0009-0002-3279-5971

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 will teach System Programming With C and Unix in Fall 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 Project Site GitHub
Parameterized Cast Calculi   GitHub

(API credit)

Refereed Articles

  • Quest Complete: the Holy Grail of Gradual Security NEW!
    Tianyu Chen, Jeremy G. Siek
    PLDI 2024 (to appear)
    DOI, PDF, PDF Full Version, Arxiv , PL Wonks, Code, Artifact (Reusable)
    artifacts_available_sm.jpg artifacts_reusable_sm.jpg
  • Parameterized Cast Calculi and Reusable Meta-theory for Gradually Typed Lambda Calculi
    Jeremy G. Siek, Tianyu Chen
    Journal of Functional Programming (JFP)
    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 (Oakland) 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

Unpublished Drafts

  • Mechanized Noninterference for Gradual Security
    Tianyu Chen, Jeremy G. Siek
    Arxiv, PDF


Instructor (On-Record) System Programming With C and Unix CSCI-C291 Fall 2024
Lead Associate Instructor Data Structures CSCI-C343 Spring 2024
Associate Instructor Data Structures (Honors) CSCI-H343 Fall 2023
Associate Instructor Systems and Protocol Security CSCI-B433, INFO-I433 Spring 2020
Associate Instructor Malware: Threat and Defense CSCI-B546, INFO-I521 Fall 2019
Associate Instructor Systems and Protocol Security CSCI-B433, INFO-I433 Spring 2019


  • Luddy PhD Instructor Award 2024 - 2025
  • Research Assistant (RA) of the Year (Computer Science Department) 2023 - 2024


  • A tool that I wrote which imports Autograder grades into Canvas in batch
  • My personal notes (require IU authentication) link
  • Some links that might be useful:
    • Indiana University academic calendar link
    • Spacemacs Agda layer link

Created: 2024-06-21 Fri 15:14