arXiv subjects

Jinhao Tan

Publications and source records attributed to Jinhao Tan.

4 recordsLinked to original sources

arXiv2026

Linking as Evaluation: Correct Separate Compilation via First-Class Environments

Separate compilation is central to modular software: components are compiled independently and linked into an executable. Separate compilation is correct when a linked program behaves like the program formed by merging its sources. This property is less routine to prove than type soundness because it requires a formal account of linking. We present $λ_{\mathsf{SCE}}$, a simply typed calculus in which linking, modules, and environments are all first-class. Programmers control module linking through a link operator, which a type-directed elaboration translates into ordinary terms of a core calculus of first-class environments. The core calculus's existing evaluation rules then perform the linking: linking as evaluation. Linking independently compiled modules yields the same core term as elaborating their source link. Therefore, compilation and linking commute by construction. As a result, separate compilation correctness follows directly from the semantics preservation for both static and dynamic linking. All meta-theory is mechanized in Lean 4, and we implement a compiler to WebAssembly in OCaml.

cs.PL↗

arXiv2026

Polymorphic First-Class Environments

First-class environments expose runtime environments as ordinary values and support a substitution-free, environment-based operational semantics. They also support applications such as first-class modules, dynamic composition of environment fragments, and sandboxing via local environments. Existing environment-based calculi, however, are mostly studied in a simply typed setting and stop short of System F and polymorphism. We present $F_E$, a polymorphic calculus with first-class environments that conservatively extends System F with a small-step environment semantics. $F_E$ eliminates all forms of substitution in System F. Term and type abstractions evaluate to closures, boxes run code under local environments, and box types expose the local typing assumptions of both. Manifest types, together with a two-sided type equivalence, play a dual role: they model type-level instantiation, and enable transparent type components in environments and modules. We prove type soundness, normalization, decidability, and standard properties of type equivalence, and conservativity over System F. The metatheory of $F_E$ is based on instantiation lemmas rather than substitution lemmas. This foundation supports polymorphic first-class modules with dynamic composition and sandboxing. We study $F_E$ in two forms. Our main presentation is an explicit, type-passing calculus that follows conventional System F. We also develop an implicitly-typed variant aligned with the semantics of polymorphic functional languages. All metatheory is mechanized in the Rocq theorem prover.

cs.PL↗

arXiv2021

BPPChecker: An SMT-based Model Checker on Basic Parallel Processes(Full Version)

Program verification on concurrent programs is a big challenge due to general undecidable results. Petri nets and its extensions are used in most works. However, existing verifiers based on Petri nets are difficult to be complete and efficient. Basic Parallel Process (BPP), as a subclass of Petri nets, can be used as a model for describing and verifying concurrent programs with lower complexity. We propose and implement BPPChecker, the first model checker for verifying a subclass of CTL on BPP. We propose constraint-based algorithms for the problem of model checking on BPPs and handle formulas by SMT solver Z3. For EF operator, we reduce the model checking of EF-formulas to the satisfiability problem of existential Presburger formula. For EG operator, we provide a k-step bounded semantics and reduce the model checking of EG-formulas to the satisfiability problem of linear integer arithmetic. Besides, we give Actor Communicating System (ACS) the over-approximation BPP-based semantics and evaluate BPPChecker on ACSs generated from real Erlang programs. Experimental results show that BPPChecker performs more efficiently than the existing tools for a series of branching-time property verification problems of Erlang programs.

cs.LO↗

arXiv2021

A novel energy resolved neutron imaging detector based on TPX3Cam for the CSNS

The China Spallation Neutron Source (CSNS) operates in pulsed mode and has a high neutron flux. This provides opportunities for energy resolved neutron imaging by using the TOF (Time Of Flight) approach. An Energy resolved neutron imaging instrument (ERNI) is being built at the CSNS but significant challenges for the detector persist because it simultaneously requires a spatial resolution of less than 100 μm, as well as a microsecond-scale timing resolution. This study constructs a prototype of an energy resolved neutron imaging detector based on the fast optical camera, TPX3Cam coupled with an image intensifier. To evaluate its performance, a series of proof of principle experiments were performed in the BL20 at the CSNS to measure the spatial resolution and the neutron wavelength spectrum, and perform neutron imaging with sliced wavelengths and Bragg edge imaging of the steel sample. A spatial resolution of 57 μm was obtained for neutron imaging by using the centroiding algorithm, the timing resolution was on the microsecond scale and the measured wavelength spectrum was identical to that measured by a beam monitor. In addition, any wavelengths can be selected for the neutron imaging of the given object, and the detector can be used for Bragg edge imaging. The results show that our detector has good performances and can satisfy the requirements of ERNI for detectors at the CSNS

physics.ins-det↗