arXiv subjects

Hongwei Xi

Publications and source records attributed to Hongwei Xi.

At least 19 recordsLinked to original sources

arXiv2026

FAST Ultra-Deep Survey: the baryonic Tully-Fisher relation in FUDS0 field

The Baryonic Tully-Fisher relation (BTFR) is one of the tightest scaling relations for disk galaxies in the local Universe, and therefore is an important tool for studying the fomation and evolution of galaxies. However, the evolution of the BTFR over cosmic time is poorly understood due to the limited sample of HI galaxies beyond the local Universe, limitations of optically-derived rotation curves, and selection effects. In this work, we explore the BTFR at redshifts up to $z=0.42$ from galaxies detected in the pilot FAST Ultra-Deep Survey (FUDS) field, FUDS0. As found in previous work, we identify two components in the plane of baryonic mass versus rotational velocity, $C_{\rm BTFR}$ (tight) and $C_{\rm Outlier}$ (dispersed). A Gaussian mixture model is employed to recover the BTFR, yielding the best fit parameters for the slope $k=3.32_{-0.11}^{+0.12}$, zero point $b=10.07_{-0.03}^{+0.03}$, and intrinsic scatter $\sigma_{\rm BTFR}=0.036_{-0.009}^{+0.010}$. A random forest classifier is used to investigate the origin of the outlier component. We find that low signal significance and inaccurate inclinations are the key factors that contribute to the outlier population, indicating that observational effects are the dominant origin. Evolutionary trends are examined in three different redshift bins. Both the slope and zero point show consistency within 1-$\sigma$ uncertainty in the two low redshift bins, indicating no significant evolution. The indirectly inferred BTFR parameters from the $C_{\rm Outlier}$ component in the highest redshift bin aligns with the conclusion. The ongoing full FUDS survey will provide a larger sample to enable more accurate constraints on BTFR evolution.

astro-ph.GA↗

arXiv2025

Dependent Session Types for Verified Concurrent Programming

We present TLLC which extends the Two-Level Linear dependent type theory (TLL) with session-based concurrency. Equipped with Martin-L\"{o}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 a form of relational verification by relating concurrent programs with their idealized sequential counterparts. Correctness properties proven for sequential programs can be easily lifted to their corresponding concurrent implementations. TLLC makes session types a powerful tool for intrinsically verifying the correctness of data structures such as queues and concurrent algorithms such as map-reduce. To extend TLL with session types, we develop a novel formulation of intuitionistic session type which we believe to be widely applicable for integrating session types into other type systems beyond the context of TLLC. We study the meta-theory of our language, proving its soundness as both a term calculus and a process calculus. To demonstrate the practicality of TLLC, we have implemented a prototype compiler that translates TLLC programs into concurrent C code, which has been extensively evaluated.

cs.PL↗

arXiv2025

FAST Ultra-Deep Survey (FUDS): the star formation histories of FUDS0 galaxies

We present the ultraviolet, optical and infrared counterparts of 128 galaxies detected in neutral hydrogen (HI) in the FAST Ultra-Deep Survey (FUDS) field 0 (FUDS0). HI mass upper limits are also calculated for 134 non-detections in the field. Stellar masses ($M_*$), star formation rates (SFRs) and star formation histories are computed by fitting spectral energy distributions (SEDs) using ProSpect. The results show that HI-selected galaxies prefer recent long-lasting, but mild star formation activity, while HI non-detections have earlier and more intense star formation activity. Based on their distribution on the SFR versus $M_*$ diagram, the typical evolution of HI-selected galaxies follows three distinct stages: (i) Early stage: the total SFR increases, though the specific SFR (sSFR) decreases from 10$^{-8}$ to 10$^{-9}$ yr$^{-1}$; (ii) Mass accumulation stage: the SFR is steady, and stellar mass increase linearly with time; (iii) Quenching stage: star formation activity quenches on a rapid timescale and at constant stellar mass. 37 non-detections are located on star-forming main sequence, but are not detected in HI due to low sensitivity close to field edges or close to strong radio frequency interference. Comparisons with the existing optical, optically-selected HI, and HI catalogs show a good agreement with respect to measured $M_*$ and SFR, with minor discrepancies due to selection effects. The ongoing full FUDS survey will help us better explore the evolutionary stages of HI galaxies through a larger sample.

astro-ph.GA↗

arXiv2024

FAST Ultra-Deep Survey (FUDS): Data Release for FUDS0

We have used the Five-hundred-meter Aperture Spherical radio Telescope (FAST) to make a blind ultra-deep survey for neutral hydrogen (HI). We present the complete results from the first of six fields (FUDS0). This observation of 95 hours allowed us to achieve a high sensitivity ($\sim 50~\mu$Jy beam$^{-1}$) and a high frequency resolution (22.9 kHz) over an area of 0.72 deg$^2$. We detected 128 galaxies in HI distributed over the redshift range of $0 0.38$, where no unlensed HI emission has previously been directly detected. Estimates of completeness and reliability are presented for the catalog. Consistency of continuum and HI flux estimates with NVSS and AUDS, respectively, confirms the accuracy of calibration method and data reduction pipeline developed for the full FUDS survey.

astro-ph.GA↗

arXiv2024

The most distant HI galaxies discovered by the 500 m dish FAST

Neutral hydrogen (HI) is the primary component of the cool interstellar medium (ISM) and is the reservoir of fuel for star formation. Owing to the sensitivity of existing radio telescopes, our understanding of the evolution of the ISM in galaxies remains limited, as it is based on only a few hundred galaxies detected in HI beyond the local Universe. With the high sensitivity of the Five-hundred-meter Aperture Spherical radio Telescope (FAST), we carried out a blind HI search, the FAST Ultra-Deep Survey (FUDS), which extends to redshifts up to 0.42 and a sensitivity of 50 $\rm \mu Jy \cdot beam^{-1}$. Here, we report the first discovery of six galaxies in HI at $z>0.38$. For these galaxies, the FAST angular resolution of $\sim\,4'$ corresponds to a mean linear size of $\sim1.3\,h_{70}^{-1}\,$Mpc. These galaxies are among the most distant HI emission detections known, with one having the most massive HI content ($10^{10.93 \pm 0.04}~h_{70}^{-2}\, \rm M_\odot$). Using recent data from the DESI survey, and new observations with the Hale, BTA, and Keck telescopes, optical counterparts are detected for all galaxies within the 3-$\sigma$ positional uncertainty ($0.5\,h_{70}^{-1}\,$Mpc) and $\rm 200\,km \cdot s^{-1}$ in recession velocity. Assuming that the dominant source of HI is the identified optical counterpart, we find an evidence of evolution in the HI content of galaxies over the last 4.2 Gyr. Our new high-redshift HI galaxy sample provides the opportunity to better investigate the evolution of cool gas in galaxies. A larger sample size in the future will allow us to refine our knowledge of the formation and evolution of galaxies.

astro-ph.GA↗

arXiv2023

A Two-Level Linear Dependent Type Theory

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 all proofs and types occurring inside programs are fully erasable without compromising their operational behavior. Through a heap-based operational semantics, we show that extracted programs always make computational progress and run memory clean. Additionally, programs can be freely reflected into the logical level for conducting deep proofs in the style of standard dependent type theories. This enables one to write resource safe programs and verify their correctness using a unified language.

cs.PL↗

arXiv2023

Multirole Logic and Multiparty Channels

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 generalized to endomorphisms on this set. We formulate both multirole logic (MRL) and linear multirole logic (LMRL) as natural generalizations of classical logic (CL) and classical linear logic (CLL), respectively. Among various meta-properties established for MRL and LMRL, we obtain one named multiparty cut-elimination stating that every cut involving one or more sequents (as a generalization of a binary cut involving exactly two sequents) can be eliminated, thus extending the celebrated result of cut-elimination by Gentzen. As a side note, we also give an ultrafilter-based interpretation for intuitionism, formulating MRLJ as a natural generalization of intuitionistic logic (IL). An immediate application of LMRL can be found in a formulation of session types for channels that support multiparty communication in distributed programming. We present a multi-threaded lambda-calculus (MTLC) where threads communicate on linearly typed multiparty channels that are directly rooted in LMRL, establishing for MTLC both type preservation and global progress. The primary contribution of the paper consists of both identifying multirole logic as a new form of logic and establishing a theoretical foundation for it, and the secondary contribution lies in applying multirole logic to the practical domain of distributed programming.

cs.LO↗

arXiv2022

The FAST Ultra-Deep Survey (FUDS): observational strategy, calibration and data reduction

The FAST Ultra-Deep Survey (FUDS) is a blind survey that aims for the direct detection of HI in galaxies at redshifts $z<0.42$. The survey uses the multibeam receiver on the Five Hundred Meter Aperture Spherical Telescope (FAST) to map six regions, each of size 0.72 deg$^2$ at high sensitivity ($\sim 50 \mu$Jy) and high frequency resolution (23 kHz). The survey will enable studies of the evolution of galaxies and their HI content with an eventual sample size of $\sim 1000$. We present the science goals, observing strategy, the effects of radio frequency interference (RFI) at the FAST site, our mitigation strategies and the methods for calibration, data reduction and imaging as applied to initial data. The observations and reductions for the first field, FUDS0, are completed, with around 128 HI galaxies detected in a preliminary analysis. Example spectra are given in this paper, including a comparison with data from the overlapping GAL2577 field of Arecibo Ultra-Deep Survey (AUDS).

astro-ph.GA↗

arXiv2020

The Arecibo Ultra-Deep Survey

The Arecibo Ultra Deep Survey (AUDS) is a blind HI survey aimed at detecting galaxies beyond the local Universe in the 21-cm emission line of neutral hydrogen (HI). The Arecibo $L$-band Feed Array (ALFA) was used to image an area of 1.35~deg$^2$ to a redshift depth of 0.16, using a total on-source integration time of over 700 hours. The long integration time and small observation area makes it one of the most sensitive HI surveys, with a noise level of $\sim 75$~$\mu$Jy per 21.4~kHz (equivalent to 4.5~km~s$^{-1}$ at redshift $z=0$). We detect 247 galaxies in the survey, more than doubling the number already detected in AUDS60. The mass range of detected galaxies is $\log(M_{\rm HI}~[h_{70}^{-2}{\rm M}_\odot]) = 6.32 - 10.76$. A modified maximum likelihood method is employed to construct an HI mass function (HIMF). The best fitting Schechter parameters are: low-mass slope $\alpha = -1.37 \pm 0.05$, characteristic mass $\log(M^*~[h_{70}^{-2}{\rm M}_\odot]) = 10.15 \pm 0.09$, and density $\Phi_* = (2.41 \pm 0.57) \times 10^{-3} h_{70}^3$~Mpc$^{-3}$~dex$^{-1}$. The sample was divided into low and high redshift bins to investigate the evolution of the HIMF. No change in low-mass slope $\alpha$ was measured, but an increased characteristic mass $M^*$, was noted in the higher-redshift sample. Using Sloan Digital Sky Survey (SDSS) data to define relative galaxy number density, the dependence of the HIMF with environment was also investigated in the two AUDS regions. We find no significant variation in $\alpha$ or $M^*$. In the surveyed region, we measured a cosmic HI density $\Omega_{\rm HI} = (3.55 \pm 0.30) \times 10^{-4} h_{70}^{-1}$. There appears to be no evolutionary trend in $\Omega_{\rm HI}$ above $2\sigma$ significance between redshifts of 0 and 0.16.

astro-ph.GA↗

arXiv2018

Implementing Linking in Multiparty Sessions (Extended Abstract)

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 are a formalism that is proposed to specify interactions between communicating processes. In essence, a session type system is a kind of type system designed to enforce (through type-checking) that the involved processes communicate according to a chosen protocol specified as a session type. It is well-known that linear logic plays a pivotal role in the study of session types. For instance, various inference rules in linear logic can be interpreted as ways for constructing channels (used by communicating processes to send/receive messages.) A particularly interesting case is the cut-rule in linear logic, which can be interpreted as a way for connecting the ends of two matching channels to form a single new channel. This form of channel construction is often referred to as linking or (bi-directional) forwarding. We have generalized classical linear logic into classical linear multirole logic (LMRL), where the former can be seen as a special case of the latter involving only two roles. In LMRL, there is a cut-rule involving multiple sequents (instead of exactly two), which we call multiparty cut (mp-cut). We have also formulated a novel multiparty session type system directly based on LMRL. When implementing it, we need to find a way of connecting multiple channels that corresponds to mp-cut. In this paper, we describe an implementation of linking for multiparty sessions in the setting of shared memory. We also describe two novel concepts, two-way linking with residual and three-way linking, which can only be formulated in the setting of multiparty sessions. Notably, linking for binary sessions can be thought of as a specially optimized version of what is implemented for multiparty sessions.

cs.PL↗

arXiv2018

To Memory Safety through Proofs

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 recently developed framework Applied Type System (ATS), the type system imposes a level of abstraction on program states through a novel notion of recursive stateful views and then relies on a form of linear logic to reason about such stateful views. We consider the design and then the formalization of the type system to constitute the primary contribution of the paper. In addition, we also mention a running implementation of the type system and then give some examples in support of the practicality of programming with recursive stateful views.

cs.PL↗

arXiv2018

Multiparty Dependent Session Types (Extended Abstract)

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 lack of formal specification/verification of concurrency. This work formalizes the first multiparty dependent session types as an expressive and practical type discipline for enforcing communication protocols. The type system is formulated in the setting of multi-threaded $\lambda$-calculus with inspirations from multirole logic, a generalization of classical logic we discovered earlier. We prove its soundness by a novel technique called deadlock-freeness reducibility. The soundness of the type system implies communication fidelity and absence of deadlock.

cs.PL↗

arXiv2017

Dependent Session Types

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 multi-threaded $\lambda$-calculus with linear types. In this work, we build upon our earlier work by presenting a form of dependent session types (of DML-style). The type system we formulate provides linearity and duality guarantees with no need for any runtime checks or special encodings. Our formulation of dependent session types is the first of its kind, and it is particularly suitable for practical implementation. As an example, we describe one implementation written in ATS that compiles to an Erlang/Elixir back-end.

cs.PL↗

arXiv2017

Applied Type System: An Approach to Practical Programming with Theorem-Proving

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 certain acute problems that make it difficult for PTS to directly accommodate many common realistic programming features such as general recursion, recursive types, effects (e.g., exceptions, references, input/output), etc. In this paper, Applied Type System (ATS) is presented as a framework for designing and formalizing type systems in support of practical programming with advanced types (including dependent types). In particular, it is demonstrated that ATS can readily accommodate a paradigm referred to as programming with theorem-proving (PwTP) in which programs and proofs are constructed in a syntactically intertwined manner, yielding a practical approach to internalizing constraint-solving needed during type-checking. The key salient feature of ATS lies in a complete separation between statics, where types are formed and reasoned about, and dynamics, where programs are constructed and evaluated. With this separation, it is no longer possible for a program to occur in a type as is otherwise allowed in PTS. The paper contains not only a formal development of ATS but also some examples taken from ats-lang.org, a programming language with a type system rooted in ATS, in support of employing ATS as a framework to formulate advanced type systems for practical programming.

cs.PL↗

arXiv2017

Multirole Logic (Extended Abstract)

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 notion of negation is generalized to endomorphisms on this underlying set. We formalize both multirole logic (MRL) and linear multirole logic (LMRL) as natural generalizations of classical logic (CL) and classical linear logic (CLL), respectively, and also present a filter-based interpretation for intuitionism in multirole logic. Among various meta-properties established for MRL and LMRL, we obtain one named multiparty cut-elimination stating that every cut involving one or more sequents (as a generalization of a (binary) cut involving exactly two sequents) can be eliminated, thus extending the celebrated result of cut-elimination by Gentzen.

math.LO↗

arXiv2017

Dependent Types for Multi-Rate Flows in Synchronous Programming

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 strict timing constraints. In this report, we encode inside ATS various real-time primitives in an experimental synchronous language called Prelude, where ATS is a statically typed language with an ML-like functional core that supports both dependent types (of DML-style) and linear types. We show that the verification requirements imposed on these primitives can be formally expressed in terms of dependent types in ATS. Moreover, we modify the Prelude compiler to automatically generate ATS code from Prelude source. This modified compiler allows us to solely rely on typechecking in ATS to discharge proof obligations originating from the need to typecheck Prelude code. Whereas ATS is typically used as a general purpose programming language, we hereby demonstrate that it can also be conveniently used to support some forms of advanced static checking in languages equipped with less expressive types.

cs.PL↗

arXiv2016

Propositions in Linear Multirole Logic as Multiparty Session Types

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-properties established for LMRL, we obtain one named multi-cut elimination stating that every cut between three (or more) sequents (as a generalization of a cut between two sequents) can be eliminated, thus extending the celebrated result of cut-elimination by Gentzen. We also present a variant of $\pi$-calculus for multiparty sessions that demonstrates a tight correspondence between process communication in this variant and multi-cut elimination in LMRL, thus extending some recent results by Caires and Pfenning (2010) and Wadler (2012), among others, along a similar line of work.

cs.PL↗

arXiv2016

Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions

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 session (i-session). As a generalization of i-session, a group session (g-session) is one in which each party may implement a group of roles based on one channel. In particular, each of the two parties involved in a dyadic g-session implements either a group of roles or its complement. In this paper, we present a formalization of g-sessions in a multi-threaded lambda-calculus (MTLC) equipped with a linear type system, establishing for the MTLC both type preservation and global progress. 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 linearly typed g-sessions in ATS. The primary contribution of the paper lies in both of the identification of g-sessions as a fundamental building block for multiparty sessions and the theoretical development in support of this identification.

cs.PL↗