Yichen Xu

semantic. Semantic Type Soundness in Lean 4

YaDNS. Yet Another DNS relay server that can be used as a local DNS over HTTPS (DoH) proxy.

cavia. Experimental compiler for capybara.

awesome-neural-code-intelligence. A curated list for awesome machine learning methods for neural code intelligence.

cdot-calculus. Soundness proof for OOPSLA 2022 paper A case for DOT: Theoretical Foundations for Objects With Pattern Matching and GADT-style Reasoning.

deeper-net. A deep learning neural network library implemented in pure C++.

dcgan. The deep convolutional generative adversarial model, written in Python, using keras with tensorflow as backend.

BrainFuckInterpreter. Yet another brain fuck interpreter implemented with pure C++.

capless-lean. Lean

met-lean4. Lean 4 mechanisation of Modal Effect Types.

YaPokemon. Yet Another Pokemon game.

mips-hike. Virtual machine of a self-designed MIPS-like instruction set, written in Haskell. A toy compiler targeting the MIPS-like assemble language is also included.

Papiers. My Experiment to create a native document management application for macOS with Swift and SwiftUI.

mltt. A tiny MLTT theorem prover

capture-calculus.lean. Lean

PointGNN. Python

warrior. Yet another scraper for jwgl.bupt.edu.cn.

CoordML. Manage ML experiments with ease. (https://github.com/CoordML)

theorem-proving-data. Collecting Github data for theorem-proving scripts.

papiers-core. Scala

fscala2c. Bring a subset of Scala to native C!

capless-website. Landing page for capture checking.

meow. A cute little library for Cats.

voter-admin. Admin for voter.

2D-Physics-Ball-System. A simple physics ball system written in pure C++.

game-system. game

space-game. A game to drive the spaceship around the planets written in ClojureScript.

lean4-medley. Lean

code-gpt-neox. Faster fine-tuning GPT for code generation.

ca-mips-lab. Computer Architecture Lab

agda-katas. Learning Agda by solving katas

travel-agency. Min-risk travel planer in COVID-19.

accumulator-verilog. A simple accumulator written in Verilog.