Formalization of the Substructural Dependent Type Theory (SStruct) in Lean 4.
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.
Experimental implementation of LSP for ATS3 in ATS3.
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.
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.
The Calculus of Inductive Linear Constructions (CILC) is a linear dependent type theory which fully formalizes the mechanism for defining linear dependent inductive types. Linear dependent inductive types allow for the language runtime to perform mutation on data which appears to be immutable from the user's perspective. The entire theory of CILC is formalized in Coq and proven to be sound. CILC is one of the few dependent inductive type systems ever formalized in a theorem prover and, to the best of our knowledge, is also the only formalized linear dependent inductive type system.
We propose a pipeline for retargeting character motion in videos by using 2 novel generative adversarial networks MT-Net and DE-Net. First, MT-Net uses of the projection of 3D human models to maintain the structural integrity of character poses during motion transfer. Next, DE-Net enhances details in generated frames by reusing the details in real source frames. This essentially eliminates the need for generating reusable details from scratch. Extensive experiments show that our approach yields better results both qualitatively and quantitatively than the state-of-the-art methods.