Liang Yalun

Education

1. BEng in Computer Science, Shanghai Jiao Tong University, Shanghai, China Sep 2021–Present

   Member of the ACM Class of SJTU. GPA: 3.97/4.3, rank: 4 of 34.

Research Experience

1. Lab. for Foundations of Computer Science, the University of Edinburgh Jul 2024–Dec 2024

   Effect handlers, undergraduate visiting research advised by Sam Lindley

   • Implemented the stack switching proposal of WebAssembly in SpecTec, a DSL for writing formal specifications for WebAssembly
   • Contributed improvements to SpecTec’s metatheory, which is now the basis of the WebAssembly 3.0 specification

2. SJTU Programming Languages and Verification Group Aug 2023–Aug 2024

   Compiler verification, undergraduate research advised by Wang Yuting

   • Worked on extensions of the CompCert verified compiler
   • Proved compiler correctness while tracing stack usage in an open-module environment

Talks

• Experience Report: Stack Switching in Wasm SpecTec Liang Yalun, Sam Lindley, and Andreas Rossberg WebAssembly Workshop 2025 at POPL 2025, January 2025

Publications

• CompCertOC: Verified Compositional Compilation of Multi-Threaded Programs with Shared Stacks Zhang Ling, Wang Yuting, Liang Yalun, and Shao Zhong PLDI 2025, June 2025
• A Coq Library of Sets for Teaching Denotational Semantics Cao Qinxiang, Wu Xiwei, and Liang Yalun Workshop on Theorem proving components for Educational software 2023 (ThEdu’23) EPTCS 400, April 2024

Teaching Experience

1. Operating Systems, teaching assistant Spring 2024

   • Designed a new lab project on virtual filesystems

2. Mathematical Logic, teaching assistant Fall 2023

   • Graded assignments and wrote sample solutions
   • Gave a review lecture at end of term with other TAs

3. Programming Practice, teaching assistant Summer 2023

   • Created problem sets for in-class exams
   • Designed a new lab project on networking

4. Data Structures, teaching assistant Spring 2023

   • Created problem sets for assignments and exams, and redesigned programming labs
   • Gave lectures on graph algorithms

5. Programming (C++), teaching assistant Fall 2022

   • Created a set of homework problems to help freshman get started on programming
   • Gave lectures on using Linux shells and Git

Selected Projects

1. Typechecker for Calculus of Inductive Constructions, course project Apr 2024–Jun 2024

   • A toy typechecker with dependent and inductive types
   • Features simple elaboration and unification processes inspired by Lean
   • Wrote some simple proofs to demonstrate its features

2. ACM Class Online Judge, programmer and operations Feb 2022–Present

   • Maintainer of online judge service, used by 9000+ students throughout the campus
   • Redesigned judge runners and the task scheduler, reworked the user interface
   • Implemented a sandbox utilizing Linux namespaces and subuids
   • Offered better security, performance and usability
   • Applied modern monitoring and observability practices to the service

3. LTL Model Checker, course project May 2024–Jun 2024

   • Implemented checking of linear temporal logic formulas via nondeterministic Büchi automata
   • Features a web UI that visualizes the checking process

4. Mx* compiler, course project Sep 2022–Feb 2023

   • Implemented a compiler for a C-like language targeting RISC-V
   • Includes various compiler optimizations

5. RISC-V CPU on FPGA, course project Nov 2022–Jan 2023

   • Implemented an out-of-order RISC-V RV32I CPU using Chisel, a Scala-based HDL.

Skills

• Programming languages: multilingual (not limited to any specific language); comfortable with Agda C C++ JavaScript Kotlin OCaml Python Rocq Scala, other languages Go Java Rust Shell Verilog.
• Natural languages: Chinese (native), English (fluent, TOEFL 111).

Miscellaneous

• I was awarded the National Scholarship of China in 2021–2022, an award given to the top 0.2% of undergraduates nationwide.
• Codeberg: https://codeberg.org/altk, my main code repository.
• GitHub: https://github.com/Alan-Liang, over 100 followers.