Source author record

Zhiqiang Ren

Zhiqiang Ren appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Programming Languages Logic in Computer Science physics.atom-ph quant-ph Software Engineering

Catalog footprint

What is connected

3works

5topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2022arXiv

Quantum Interference between Photons and Single Quanta of Stored Atomic Coherence

Essential for building quantum networks over remote independent nodes, the indistinguishability of photons has been extensively studied by observing the coincidence dip in the Hong-Ou-Mandel interferometer. However, indistinguishability is not limited to the same type of bosons. For the first time, we hereby observe quantum interference between flying photons and a single quantum of stored atomic coherence (magnon) in an atom-light beam splitter interface. We demonstrate that the Hermiticity of this interface determines the type of quantum interference between photons and magnons. Consequently, not only the bunching behavior that characterizes bosons is observed, but counterintuitively, fermionlike antibunching as well. The hybrid nature of the demonstrated magnon-photon quantum interface can be applied to versatile quantum memory platforms, and can lead to fundamentally different photon distributions from those occurring in boson sampling.

preprint2016arXiv

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.

preprint2012arXiv

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.