arXiv subjects

Hongwei Xi

Publications and source records attributed to Hongwei Xi.

21 records · Page 2Linked to original sources

arXiv2016

Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus

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 global progress. The latter (global progress) implies that the evaluation of a well-typed program in the MTLC can never reach a deadlock. As this formulated MTLC can be readily embedded into ATS, a full-fledged language with a functional programming core that supports both dependent types (of DML-style) and linear types, we obtain a direct implementation of session types in ATS. In addition, we gain immediate support for a form of dependent session types based on this embedding into ATS. Compared to various existing formalizations of session types, we see the one given in this paper is unique in its closeness to concrete implementation. In particular, we report such an implementation ready for practical use that generates Erlang code from well-typed ATS source (making use of session types), thus taking great advantage of the infrastructural support for distributed computing in Erlang.

cs.PL↗

arXiv2015

A robust and efficient method for estimating enzyme complex abundance and metabolic flux from expression data

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 localization of enzyme complexes, with highthroughput data including expression data, metabolomics, or DNA sequencing. The desired result is to increase predictive capability resulting in improved understanding of metabolism. The approach typically employed when only gene (or protein) intensities are available is the creation of tissue-specific models, which reduces the available reactions in an organism model, and does not provide an objective function for the estimation of fluxes, which is an important limitation in many modeling applications. We develop a method, flux assignment with LAD (least absolute deviation) convex objectives and normalization (FALCON), that employs metabolic network reconstructions along with expression data to estimate fluxes. In order to use such a method, accurate measures of enzyme complex abundance are needed, so we first present a new algorithm that addresses quantification of complex abundance. Our extensions to prior techniques include the capability to work with large models and significantly improved run-time performance even for smaller models, an improved analysis of enzyme complex formation logic, the ability to handle very large enzyme complex rules that may incorporate multiple isoforms, and depending on the model constraints, either maintained or significantly improved correlation with experimentally measured fluxes. FALCON has been implemented in MATLAB and ATS, and can be downloaded from: https://github.com/bbarker/FALCON. ATS is not required to compile the software, as intermediate C source code is available, and binaries are provided for Linux x86-64 systems. FALCON requires use of the COBRA Toolbox, also implemented in MATLAB.

q-bio.MN↗

arXiv2012

A Programmer-Centric Approach to Program Verification in ATS

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. While there is already a vast body of work on software testing and verification, the task to ensure that an implementation indeed meets its specification is still undeniably of great difficulty. ATS is a programming language equipped with a highly expressive type system that allows the programmer to specify and implement and then verify within the language itself that an implementation meets its specification. In this paper, we present largely through examples a programmer-centric style of program verification that puts emphasis on requesting the programmer to explain in a literate fashion why his or her code works. This is a solid step in the pursuit of software construction that is verifiably correct according to specification.

cs.PL↗