31 citations · 51 across the 14 of their papers we have counts for
15 papers
Dependent Session Types for Verified Concurrent Programming
Qiancheng Fu, Hongwei Xi, Ankush Das
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…
Multirole Logic and Multiparty Channels
Hongwei Xi, Hanwen Wu
We identify multirole logic as a new form of logic in which conjunction/disjunction is interpreted as an ultrafilter on some underlying set of roles and the notion of negation is g…
A Two-Level Linear Dependent Type Theory
Qiancheng Fu, Hongwei Xi
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 pr…
To Memory Safety through Proofs
Hongwei Xi, Dengping Zhu
We present a type system capable of guaranteeing the memory safety of programs that may involve (sophisticated) pointer manipulation such as pointer arithmetic. With its root in a…
Implementing Linking in Multiparty Sessions (Extended Abstract)
Hanwen Wu, Hongwei Xi
The fast growth of service-oriented programming (SOP) is evident in this day and age of the Internet, and handling communication is of paramount importance in SOP. Session types ar…
Multiparty Dependent Session Types (Extended Abstract)
Hanwen Wu, Hongwei Xi
Programs are more distributed and concurrent today than ever before, and structural communications are at the core. Constructing and debugging such programs are hard due to the lac…
Dependent Session Types
Hanwen Wu, Hongwei Xi
Session types offer a type-based discipline for enforcing communication protocols in distributed programming. We have previously formalized simple session types in the setting of m…
Applied Type System: An Approach to Practical Programming with Theorem-Proving
Hongwei Xi
The framework Pure Type System (PTS) offers a simple and general approach to designing and formalizing type systems. However, in the presence of dependent types, there often exist…
Multirole Logic (Extended Abstract)
Hongwei Xi, Hanwen Wu
We identify multirole logic as a new form of logic in which conjunction/disjunction is interpreted as an ultrafilter on the power set of some underlying set (of roles) and the noti…
Dependent Types for Multi-Rate Flows in Synchronous Programming
William Blair, Hongwei Xi
Synchronous programming languages emerged in the 1980s as tools for implementing reactive systems, which interact with events from physical environments and often must do so under…
Propositions in Linear Multirole Logic as Multiparty Session Types
Hongwei Xi, Hanwen Wu
We identify multirole logic as a new form of logic and formalize linear multirole logic (LMRL) as a natural generalization of classical linear logic (CLL). Among various meta-prope…
Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions
Hongwei Xi, Hanwen Wu
Traditionally, each party in a (dyadic or multiparty) session implements exactly one role specified in the type of the session. We refer to this kind of session as an individual se…
Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus
Hongwei Xi, Zhiqiang Ren, Hanwen Wu +1
We present a formalization of session types in a multi-threaded lambda-calculus (MTLC) equipped with a linear type system, establishing for the MTLC both type preservation and glob…
A robust and efficient method for estimating enzyme complex abundance and metabolic flux from expression data
Brandon Barker, Narayanan Sadagopan, Yiping Wang +5
A major theme in constraint-based modeling is unifying experimental data, such as biochemical information about the reactions that can occur in a system or the composition and loca…
A Programmer-Centric Approach to Program Verification in ATS
Zhiqiang Ren, Hongwei Xi
Formal specification is widely employed in the construction of high-quality software. However, there is often a huge gap between formal specification and actual implementation. Whi…