Type Theory & Verification

Substructural Dependent Type Theory

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

Probabilistic Refinement Session Types

We develop a novel theory of probabilistic refinement session types (PReST) to symbolically specify and reason about probabilistic message passing concurrent programs. The soundness of the PReST type system ensures that the probabilistic distributions specified in communication protocols are respected at runtime. Most surprisingly, probabilistic refinement types can even be used to statically verify parametric distributions such as the uniform distribution over {0, ..., k}. Using PReST we are able to specify probabilistic distributed protocols such as Leader Election, Bounded Retransmission and Crowd Forwarding. We implement a type checker in OCaml using Z3 and CVC5 to efficiently solve complex generated constraints.

Two-Level Linear Dependent Type Theory

The Two-Level Linear (TLL) dependent type theory is a programming language which combines dependent types and linear types. TLL features full Martin-Löf style dependent types to precisely reason about linearly typed programs. We fully verify the theory of TLL in Coq. A prototype optimizing compiler is implemented. It emits safe C code that is memory clean without need of runtime garbage collection. We also extend the compiler with features such as dependent session types for concurrency and sort-polymorphic schemes to write code generically for both linear and unrestricted types.

Calculus of Inductive Linear Constructions

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

Algebraic Formal Methods

🚧 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. In particular, the core constructions of rs-wspp are backed by the Lean formalization.

On-the-fly GKAT

The theory of Kleene Algebra with Tests (KAT) allows one to decide the equivalence of imperative programs using an elegant equational theory. The theory of Guarded Kleene Algebra with Tests (GKAT) promises to improve the performance of KAT by restricting its scope to the deterministic fragment of KAT. In practice, however, GKAT decision algorithms tend to be even slower than KAT algorithms due to the necessity of performing additional normalization steps. To solve the issue of using GKAT in practice, we introduce a novel on-the-fly algorithm for GKAT which performs bisimulation in a greedy manner and defers normalization to when it is absolutely necessary. We develop the rust-gkat tool in Rust. Through experiments, we show that our tool performs orders of magnitudes faster than existing KAT solvers.

Tools & Applications

Autosubst for Lean 4

A Lean 4 port of Autosubst 2 which generates de Bruijn substitution boilerplate for programming language formalizations.

ATS3 Language Server Protocol

Experimental implementation of LSP for ATS3 in ATS3.

Motion Transfer and Detail Enhancement Neural Networks

Pipeline for retargeting character motion in videos by using 2 novel generative adversarial networks MT-Net and DE-Net.