Tianchuan Lin (林田川)
![](/me.jpg)
I am a third-year undergraduate student of Computer Science at ACM Class, Shanghai Jiao Tong University.
I am interested in Formal Verification, Programming Languages and Distributed Systems. I achieved A+ in the following courses: Programming Verification, Mathematical Logic, Compiler Design and Implementation, Distributed Systems.
- Email: [email protected]
- Github: 1024th
Research Interests
I am interested in building reliable and efficient software systems.
Formal methods are a powerful tool for building reliable software. They can be used to prove that software is correct. However, formal methods are not widely used because they require a lot of human effort and expertise. How to make formal methods more accessible and practical attracts me.
I am also interested in optimizing the performance of software systems, especially for Machine Learning and Distributed Systems. I am fascinated by the practical ideas and techniques that can be used to improve the performance of software systems.
Projects
- Correctness Verification of the Use/Def Analysis: Course project of CS 2206, Programming Verification.
We use Coq to define and prove the correctness of the Use/Def analysis of a simple programming language. We also prove the equivalence of two different iterative algorithms for the analysis. - Google File System (Github): Course project of Distributed Systems, 2023 Summer.
Google File System is a distributed file system developed by Google. This project is a simplified implementation of GFS, written in Go. - Mx-Compiler (Github): Course Project of Compiler Design and Implementation.
A compiler for Mx* language, a subset of C/Java. The compiler is written in Java and generates RISC-V assembly code. LLVM IR is used as the intermediate representation.
Some optimizations are implemented, including Aggressive Dead Code Elimination, Loop Invariant Code Motion, etc. - Distributed Hash Table (GitHub): Course project of PPCA 2022 DHT.
Two protocols are implemented: Chord and Kademlia. An application layer is built on top of the protocols to provide file sharing service similar to BitTorrent. The project is written in Go. - Fine-tuning Transformer Model for Trickier Symbolic Integration: Course project of Machine Learning.
Based on Facebook AI's ‘Deep Learning for Symbolic Mathematics’, we fine-tune the model to solve trickier symbolic integrals. - RV32I CPU (Github): Course project of Computer Architecture.
A Tomasulo-based out-of-order CPU with Instruction Cache and Branch Prediction. The CPU is written in Verilog and executed on FPGA.
Experience
- Mathematical Logic (Fall 2023), Teaching Assistant. The syllabus is similar to previous year.
- Programming Practice 2023, Teaching Assistant. I improved the course project Distribute Hash Table.
- Programming (C++) 2022, Teaching Assistant. I improved the course project.
- CCF Certified Software Professional - Senior (CSP-S) 2019, the first prize in province.
CSP-S is equivalent to National Olympiad in Informatics in Provinces (NOIP). CCF is the abbreviation of China Computer Federation.
Skills
- Programming Languages: C/C++, Java, Python, Go, Verilog, Coq, Dafny.
- Tools: Git, Linux, Vim, SSH, LaTeX.