Hi Matthew
Sorry to be so slow in responding: things are very busy just at the moment.
Matthew Sackman wrote:
I have wondering
about dependant types and concurrency, wrt epigram, in particular,
whether dependant types in the style of epigram could mean that given
constructors for parallelism, you could harness the type system to
prevent ever being able to construct race-conditions or deadlocks.
Interesting question... wish I knew the answer.
Have you looked at this area at all or have any comments?
I haven't looked at this area, but it's certainly worth thinking about.
Certainly, people have used dependent type theory to model process
calculi and verify properties of the processes they express, and there's
been quite a bit of work on interfacing proof assistants and model
checkers. I don't know of any work which tries to be more exact about
the processes constructable in the first place.
To make any such thing practicable, we'd need at least
(A) coinductive datatypes, to model infinite behaviour,
(B) quotient types, to model sets of behaviour and behavioural
equivalence (eg between different interleavings).
Type systems for concurrent processes use types to express the
capabilities of those processes, so one can imagine using typed
processes to demand the absence of the deadlocking capability, or some
such. Whether these properties are just too complex to internalise in
types, it's just too early to say.
Epigram 1 doesn't support either (A) or (B), but both are scheduled to
appear in Epigram 2.
Things worth looking at include:
Peter Hancock, Pierre Hyvernat and Anton Setzer's work on modelling
interaction in type theory;
Eduardo Gimenez's work on coinduction in Coq (and, more generally,
coinduction in Coq);
Frank Pfenning, Kevin Watkins et al on the Concurrent Logical Framework.
Any more for any more?
All the best
Conor
