Tianyu Chen

• 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

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 teach CSCI-C291 "System Programming With C and Unix". Here is my course website of Fall 2024. In the foreseeable future, Spring 2025 will be the last semester during which my version of C291 is offered at IU.

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.

• Quest Complete: the Holy Grail of Gradual Security
  Tianyu Chen, Jeremy G. Siek
  PLDI 2024
  DOI, PDF, PDF Full Version, Arxiv , PL Wonks, Code, Artifact (Reusable)
  
• 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
  DOI
• Characterizing Smartwatch Usage in the Wild
  Xing Liu, Tianyu Chen, Feng Qian, Zhixiu Guo, Felix Xiaozhu Lin, Xiaofeng Wang, Kai Chen
  MobiSys 2017
  DOI
• Paxos Made Transparent
  Heming Cui, Rui Gu, Cheng Liu, Tianyu Chen, Junfeng Yang
  SOSP 2015
  DOI

• Generic Blame-Subtyping Theorem in Agda Using Abstract Binding Trees
  Tianyu Chen
  POPL 2022 Student Research Competition
  Extended abstract, Poster, Certificate

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

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

• 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
  • Indiana University final exam schedule and policies link
  • Indiana University final grade submission policy link
  • Spacemacs Agda layer link

• This page is written in org-mode and published to HTML.