2026
A Two-Level Linear Dependent Type Theory
Qiancheng Fu, Hongwei Xi
ACM Transactions on Computational Logic 2026 [Paper]
We present a type theory combining both linearity and dependency by stratifying typing rules into a level for logics and a level for programs. The distinction between logics and programs decouples their semantics, allowing the type system to assume tight resource bounds. A natural notion of irrelevancy is established where...
A Two-Level Linear Dependent Type Theory
Qiancheng Fu, Hongwei Xi
ACM Transactions on Computational Logic 2026 [Paper]
We present a type theory combining both linearity and dependency by stratifying typing rules into a level for logics and a level for programs. The distinction between logics and programs decouples their semantics, allowing the type system to assume tight resource bounds. A natural notion of irrelevancy is established where...
Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
Cheng Zhang, Qiancheng Fu, Hang Ji, Ines Santacruz Del Valle, Alexandra Silva, Marco Gaboardi
European Symposium on Programming 2026 [Paper]
This paper presents several efficient decision procedures for trace equivalence of GKAT automata, which make use of on-the-fly symbolic techniques via SAT solvers. To demonstrate applicability of our algorithms, we designed symbolic derivatives for CF-GKAT, a practical system based on GKAT designed to validate control-flow transformations. We implemented the algorithms...
Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
Cheng Zhang, Qiancheng Fu, Hang Ji, Ines Santacruz Del Valle, Alexandra Silva, Marco Gaboardi
European Symposium on Programming 2026 [Paper]
This paper presents several efficient decision procedures for trace equivalence of GKAT automata, which make use of on-the-fly symbolic techniques via SAT solvers. To demonstrate applicability of our algorithms, we designed symbolic derivatives for CF-GKAT, a practical system based on GKAT designed to validate control-flow transformations. We implemented the algorithms...
2025
Dependent Session Types for Verified Concurrent Programming
Qiancheng Fu, Hongwei Xi
arXiv 2025 [Paper]
We present TLLC which extends the Two-Level Linear dependent type theory (TLL) with session-based concurrency. Equipped with Martin-Löf style dependency, the session types of TLLC allow protocols to specify properties of communicated messages. When used in conjunction with the dependent type machinery already present in TLL, dependent session types facilitate...
Dependent Session Types for Verified Concurrent Programming
Qiancheng Fu, Hongwei Xi
arXiv 2025 [Paper]
We present TLLC which extends the Two-Level Linear dependent type theory (TLL) with session-based concurrency. Equipped with Martin-Löf style dependency, the session types of TLLC allow protocols to specify properties of communicated messages. When used in conjunction with the dependent type machinery already present in TLL, dependent session types facilitate...
Probabilistic Refinement Session Types
Qiancheng Fu, Ankush Das, Marco Gaboardi
ACM SIGPLAN Conference on Programming Language Design and Implementation 2025 [Paper]
Session types provide a formal type system to define and verify communication protocols between message-passing processes. In order to analyze randomized systems, recent works have extended session types with probabilistic type constructors. Unfortunately, all the proposed extensions only support constant probabilities which limits their applicability to real-world systems. Our work...
Probabilistic Refinement Session Types
Qiancheng Fu, Ankush Das, Marco Gaboardi
ACM SIGPLAN Conference on Programming Language Design and Implementation 2025 [Paper]
Session types provide a formal type system to define and verify communication protocols between message-passing processes. In order to analyze randomized systems, recent works have extended session types with probabilistic type constructors. Unfortunately, all the proposed extensions only support constant probabilities which limits their applicability to real-world systems. Our work...
2023
A Two-Level Linear Dependent Type Theory
Qiancheng Fu, Hongwei Xi
arXiv 2023 [Paper]
We present a type theory combining both linearity and dependency by stratifying typing rules into a level for logics and a level for programs. The distinction between logics and programs decouples their semantics, allowing the type system to assume tight resource bounds. A natural notion of irrelevancy is established where...
A Two-Level Linear Dependent Type Theory
Qiancheng Fu, Hongwei Xi
arXiv 2023 [Paper]
We present a type theory combining both linearity and dependency by stratifying typing rules into a level for logics and a level for programs. The distinction between logics and programs decouples their semantics, allowing the type system to assume tight resource bounds. A natural notion of irrelevancy is established where...
A Dependently Typed Language with Dynamic Equality
Mark Lemay, Qiancheng Fu, William Blair, Cheng Zhang, Hongwei Xi
Workshop on Type-Driven Development 2023 [Paper]
Dependent type systems are powerful tools for preventing bugs in programs. Unlike other formal methods, dependent type systems can reuse the methodology and syntax familiar to functional programmers to construct formal proofs. However, usability issues, like confusing error messages, often arise from the conservative equalities required by such type theories....
A Dependently Typed Language with Dynamic Equality
Mark Lemay, Qiancheng Fu, William Blair, Cheng Zhang, Hongwei Xi
Workshop on Type-Driven Development 2023 [Paper]
Dependent type systems are powerful tools for preventing bugs in programs. Unlike other formal methods, dependent type systems can reuse the methodology and syntax familiar to functional programmers to construct formal proofs. However, usability issues, like confusing error messages, often arise from the conservative equalities required by such type theories....
A Calculus of Inductive Linear Constructions
Qiancheng Fu, Hongwei Xi
Workshop on Type-Driven Development 2023 [Paper]
In this paper, we present a novel calculus of inductive linear constructions (CILC), combining linear types and dependent types. Our type theory addresses a looming issue in the research on linear dependent types: the lack of a general mechanism for defining sound linear inductive types. CILC allows one to encode...
A Calculus of Inductive Linear Constructions
Qiancheng Fu, Hongwei Xi
Workshop on Type-Driven Development 2023 [Paper]
In this paper, we present a novel calculus of inductive linear constructions (CILC), combining linear types and dependent types. Our type theory addresses a looming issue in the research on linear dependent types: the lack of a general mechanism for defining sound linear inductive types. CILC allows one to encode...
2022
Human Motion Transfer With 3D Constraints and Detail Enhancement
Yangtian Sun, Qiancheng Fu, Yueren Jiang, Zitao Liu, Yukun Lai, Hongbo Fu, Lin Gao
IEEE Transactions on Pattern Analysis and Machine Intelligence 2023 [Paper]
We propose a new method for realistic human motion transfer using a generative adversarial network (GAN), which generates a motion video of a target character imitating actions of a source character, while maintaining high authenticity of the generated results. We tackle the problem by decoupling and recombining the posture information...
Human Motion Transfer With 3D Constraints and Detail Enhancement
Yangtian Sun, Qiancheng Fu, Yueren Jiang, Zitao Liu, Yukun Lai, Hongbo Fu, Lin Gao
IEEE Transactions on Pattern Analysis and Machine Intelligence 2023 [Paper]
We propose a new method for realistic human motion transfer using a generative adversarial network (GAN), which generates a motion video of a target character imitating actions of a source character, while maintaining high authenticity of the generated results. We tackle the problem by decoupling and recombining the posture information...
2021
Gradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
Mark Lemay, Qiancheng Fu, Hongwei Xi
Workshop on Type-Driven Development 2021 [Paper]
Dependent type systems are powerful tools to eliminate bugs from programs. Unlike other systems of formal methods, dependent type systems can re-use the methodology and syntax that functional programmers are already familiar with for the construction of formal proofs. However, implementations of these languages still have substantial usability issues arising...
Gradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
Mark Lemay, Qiancheng Fu, Hongwei Xi
Workshop on Type-Driven Development 2021 [Paper]
Dependent type systems are powerful tools to eliminate bugs from programs. Unlike other systems of formal methods, dependent type systems can re-use the methodology and syntax that functional programmers are already familiar with for the construction of formal proofs. However, implementations of these languages still have substantial usability issues arising...