Lucian Wischik's Research.

I am interested in the theory and implementation of the pi calculus. The challenge is that, with current technologies, it takes too much mental effort on the part of programmers to understand concurrency (threads, mutexes, events). I believe that a new sort of language based on message-passing would be easier. I work for Microsoft in Seattle.


Old Names for Nu (L Wischik; Dagstuhl Seminar 04241) - The restriction operator records 'old' names - ones that have already been created. This is neither desirable in an implementation, nor needed in the pi calculus. [download pdf] [full details] [bibtex]
A reliable protocol for synchronous rendezvous (note) (L Wischik, D Wischik; Bologna TR-2004-1) - Asynchronous rendezvous is often said to be better for distributed systems. It's not. Here we give a reliable protocol for synchronous rendezvous, and prove it correct with a novel Markov-Process technique. [download pdf] [full details] [bibtex]
A process calculus of atomic commit (L Bocchi, L Wischik; WS-FM 2004) - Atomic commit and synchronous rendezvous are one and the same. [download pdf] [full details] [bibtex]
Strong bisimulation for the explicit fusion calculus (L Wischik, P Gardner; FOSSACS 2004) - Explicit fusions give a more natural definition of Sangiorgi's "open bisimulation", and make the basic congruences coincide (whereas they don't in the synchronous pi calculus without explicit fusions). [download pdf] [full details] [bibtex]
Linear forwarders (P Gardner, C Laneve, L Wischik; CONCUR 2003) - Linear forwarders make for an easy distributed implementation of the asynchronous pi calculus, through a direct encoding of its "input capability". [download pdf] [full details] [bibtex]
New directions in implementing the pi calculus (L Wischik; Cabernet Workshop 2002) - An argumentative position-paper: the pi calculus is commercially useful, but it shouldn't be implemented with ambients or with the restriction operator. [download pdf] [full details] [bibtex]
Explicit fusions: theory and implementation (L Wischik; PhD dissertation 2001) - Theory: several strong bisimulation congruences coincide for explicit fusions, and can be 'efficiently' characterised in the style of Sangiorgi's open bisimulation. Implementation: a simple distributed abstract machine for the pi calculus and explicit fusion calculus, with proofs of its correctness and efficiency. [download pdf] [full details] [bibtex]
The fusion machine (extended abstract) (P Gardner, C Laneve, L Wischik; CONCUR 2002) - A simple distributed abstract machine for implementing pi-like calculi. Closely related to the calculi, so allowing strong correctness results. A bit like the machine inside Pict, but distributed. [download pdf] [full details] [bibtex]
Explicit Fusions (P Gardner, L Wischik; to appear in TCS; extended abstract in MFCS 2000) - An explicit fusion x=y is a persistent process which allows two names to be used interchangeably. Explanation, and some bisimulation results. Also full abstraction with fusion calculus. [download pdf] [extended abstract pdf] [full details] [bibtex]
Symmetric action calculi (extended abstract) (L Wischik, P Gardner; EXPRESS'99) - A symmetric version of Milner's action calculi. Closer to category theory than to process calculi, but it inspired our later work on explicit fusions. [extended abstract pdf] [unpublished full version] [a graphical proof tool] [full details] [bibtex]
Verifying arbitrary temporal formulas in the Temporal Logic of Actions (L Wischik; in SRC tech note 1999-003) - How I used and adapted the tableau method (Clark & Emerson) for TLA as a summer intern at SRC. [download pdf] [full details] [bibtex]

Other documents

Fusions overview (L Wischik) - Much of my research has been on the use of fusions to help with the theory and implementation of such the pi calculus. I have since disowned them, since they seem too hard to implement. [overview of fusions]
Process calculi for web choreography (L Wischik) - The W3C Web Services Choreography Group is interested in the pi calculus. This is a talk I gave to the group's inaugural meeting. [download pdf] [full details]
Fusion machine online prototype (L Wischik) - An implementation of the pi calculus, show-casing the use of explicit fusions. [use it online] [bibtex]
Film at Compaq SRC (L Wischik et al; 1999) - Each summer, the interns at Compaq SRC make a short film. In my year, I directed it! [production notes online]