Projects - Qiancheng Fu

Work in progress

The O₃ Programming Language

O₃ is a high performance functional programming language based on the SStruct dependent type theory. High-level optimizations guided by the advanced substructural type system allow O₃ to achieve native performance without GC. This project...

qcfu-bu/SStructTT

Substructural Dependent Type Theory

Formalization of the Substructural Dependent Type Theory (SStruct) in Lean 4.

View code

10.5281/zenodo.15151161

Probabilistic Refinement Session Types

A novel theory of probabilistic refinement session types (PReST) to symbolically specify and reason about probabilistic message-passing concurrent programs. Its soundness ensures the distributions specified in communication protocols are respected at runtime, and refinement...

View artifact

10.5281/zenodo.20328342

Two-Level Linear Dependent Type Theory

A programming language combining dependent and linear types. TLL features full Martin-Löf style dependent types to precisely reason about linearly typed programs, and is fully verified in Coq. A prototype optimizing compiler emits safe...

View artifact

qcfu-bu/CLC

Calculus of Inductive Linear Constructions

Formalization and implementation of Calculus of Inductive Linear Constructions (CILC).

View code

Work in progress

Weighted Symbolic Packet Programs

Formalization of Weighted Symbolic Packet Programs (WSPP) algorithms in Lean 4 for efficient representation and queries of Weighted NetKAT. A Rust version (rs-wspp) with cutting-edge performance is also implemented, with its core constructions backed...

10.5281/zenodo.18304183

On-the-fly GKAT

Guarded Kleene Algebra with Tests (GKAT) promises faster equivalence checking than KAT, but its decision algorithms are often slower in practice due to normalization overhead. We introduce a novel on-the-fly algorithm that performs bisimulation...

View artifact

qcfu-bu/lean-autosubst