# Hanwen Wu

## Contact Details

NameHanwen Wu |
||

Affiliation |
||

Location |
||

## Pubs By Year |
||

## Pub CategoriesComputer Science - Programming Languages (4) Computer Science - Logic in Computer Science (3) Computer Science - Distributed; Parallel; and Cluster Computing (1) Mathematics - Logic (1) |

## Publications Authored By Hanwen Wu

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. Read More

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. Read More

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. Read More

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. Read More