Tianyu Chen

Profile picture: Show

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

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 was a software verification intern at CertiK during summer 2021 . I worked on certifying the functional correctness of system software using Coq and CompCert.

I organize the Programming Languages Reading Group (PLRG@IU). Please refer to our website if you are interested in attending! Feel free to send me an email if you have questions.

Gradual Security Typing	link
Parameterized Cast Calculi	link

• Mechanized Noninterference for Gradual Security NEW!
  Tianyu Chen, Jeremy G. Siek
  Draft in submission
  Arxiv PDF Code
• 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

• Generic Blame-Subtyping Theorem in Agda Using Abstract Binding Trees
  Tianyu Chen
  Selected as a participant in POPL 2022 Student Research Competition
  Extended abstract Poster

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

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

---

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