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]
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]
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]
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]