The paper investigates a concurrent computation model, chi calculus, in which communications resemble cut eliminations for classical proofs. Two bisimilarities, local bisimilarity and barbed bisimilarity, on chi processes are studied and are shown to be congruence relations. The former equivalence turns out to be strictly stronger than the latter. It is shown that chi calculus is capable of modeling sequential computation in that it captures the operational semantics of call-by-name lambda calculus. A translation from pi calculus to chi calculus is given, demonstrating that, practically speaking, pi is a sublanguage of chi. A higher order version of chi calculus is proposed and examined. It combines the communication mechanism of chi calculus and the recursion mechanism of full lambda calculus, and therefore extends both.

The paper investigates the non-symbolic algebraic semantics of the weak bisimulation congruences on finite pi processes. The weak bisimulation congruences are studied both in the absence and in the presence of the mismatch operator. Some interesting phenomena about the open congruences are revealed. Several new tau laws are discovered and their relationship is discussed. The contributions of the paper are mainly as follows: 1. It is proved that Milner's three tau laws fail to lift a complete system for the strong open congruence to a complete system for the weak open congruence in the absence of both the mismatch operator and the restriction operator. A fourth tau law is proposed to deal with the match operator under the prefix operation. It is shown that for this calculus a complete system for the strong open congruence extended with all the four tau laws is complete for the weak open congruence. 2. It is verified that the four tau laws are also enough for the weak open congruence of the picalculus without the mismatch operator. Two complete systems are given, one using distinctions and the other using a schematic law for the restriction operator. 3. It is pointed out that the standard definition of the weak open congruence gives rise to a bad equivalence relation in the presence of the mismatch operator. Two alternatives are proposed. These are the late open congruence and the early open congruence. Their difference is similar to that between the weak late congruence and the weak early congruence. Complete axiomatic systems for the two weak open congruences are given.

In this paper we define a logical framework, called λTT, that is well-suited for semantic analysis. We introduce the notion of a fibration L1: T1→C1 being internally definable1 in a fibration L2: T2→C2. This notion amounts to distinguishing an internal category L in L2 and relating L1 to the externalization of L through a pullback. When both L1 and L2 are term models of typed calculi L1 and L2 respectively, we say that L1 is an internal typed calculus definable in the frame language L2. We will show by examples that if an object language is adequately represented in λTT, then it is an internal typed calculus definable in the frame language λTT. These examples also show a general phenomenon: if the term model of an object language has categorical structure S, then an adequate encoding of the language in λTT imposes an explicit internal categorical structure S in the term model of λTT and the two structures are related via internal definability. Our categorical investigation of logical frameworks indicates a sensible model theory of encodings.

Chi calculus was proposed as a process calculus that has a uniform treatment of names. Preliminary properties of chi calculus have been examined in literature. In this paper a more systematic study of bisimilarities for chi processes is carried out. The notion of L-bisimilarity is introduced to give a possible classification of bisimilarities on chi processes. It is shown that the set of L-bisimilarities form a four element lattice and that well-known bisimilarities for chi processes fit into the lattice hierarchy. The four distinct L-bisimilarities give rise to four congruence relations. Complete axiomatization system is given for each of the four congruences.

The definition of open bisimilarity on the χ-processes does not give rise to a sensible relation on the χ-processes with the mismatch operator. The paper proposes ground open congruence as a principal open congruence on the χ-processes with the mismatch operator. Thealgebraic properties of the ground congruence is studied. The paper also takes a close look at barbed congruence. This relation is similar to the ground congruence. The precise relationship between the two is worked out. It is pointed out that the sound and complete system for the ground congruence can be obtained by removing one tau law from the complete system for the barbed congruence.

We give an interpretation of Martin-L

The theory of chi processes with the mismatch operator is studied. Two open congruence relations are investigated. These are weak early open congruence and weak late open congruence. Complete systems are given for both congruence relations. These systems use some new tau laws. The results of this paper correct some popular mistakes in literature.

The paper carries out a systematic investigation into the axiomatization problem of the asymmetric chi calculus. As a crucial step in attacking the problem, an open style bisimilarity is defined for each of the eighteen L-bisimilarities and the two are proved to be equal. On top of the open bisimilarities, explicit definitions of the eighteen L-congruences are given, which suggest immediately possible axioms for the congruence relations. In addition to the axioms for strong bisimilarity, the paper proposes altogether twenty one additional axioms, three of which being the well-known tau laws and the other eighteen being new. These axioms help to lift a complete system for the strong bisimilarity to complete systems for the eighteen L-congruences.

Chi calculus was proposed as a process algebra that has a uniform treatment of names. The paper carries out a systematic study of bisimilarities for chi processes. The notion of L-bisimilarity is introduced to give a possible classification of bisimilarities on chi processes. It is shown that the set of L-bisimilarities forms a four element lattice and that well-known bisimilarities for chi processes fit into the lattice hierarchy. The four distinct L-bisimilarities give rise to four congruence relations. Complete axiomatization system is given for each of the four relations. The bisimulation lattice of asynchronous chi processes and that of asymmetric chi processes are also investigated. It turns out that the former consists of two elements while the latter twelve elements. Finally it is pointed out that the asynchronous asymmetric chi calculus has a bisimulation lattice of eight elements.

The paper proposes a new process algebra, called χ-calculus. The language differs from π-calculus in several aspects. First it takes a more uniform view on input and output. Second, the closed names of the language is homogeneous in the sense that there is only one kind of bound names. Thirdly, the effects of communications in χ-calculus are delimited by localization operators, not by sequentiality combinator. Finally, the language cherishes more freedom of parallelism than x-calculus. The algebraic properties of χ-processes are studied in terms of local bisimulation. It is shown that local bisimilarity is a congruence equivalence on χ-processes.