Open AccessConstraints for Polymorphic Behaviours of Concurrent ML
Author(s) -
Flemming Nielson,
Hanne Riis Nielson
Publication year - 1995
Publication title -
daimi pb
Language(s) - English
Resource type - Journals
eISSN - 2245-9316
pISSN - 0105-8517
DOI - 10.7146/dpb.v24i496.7024
Subject(s) - concurrency , unification , soundness , construct (python library) , process calculus , statement (logic) , computer science , algebraic number , algebra over a field , principal (computer security) , mathematics , programming language , theoretical computer science , pure mathematics , epistemology , mathematical analysis , philosophy , operating system
We present a type and behaviour reconstruction algorithm for Standard ML with concurrency. The behaviours express the communication effects during execution and resemble terms of a process algebra. The algorithm uses unification for the (essentially) free algebra of types and algebraic reconstruction for collecting constraints for the non-free algebra of behaviours. The algorithm and the statement and proof of soundness are designed so as to make no assumptions on the existence of ``principal´´ behaviours as these are unlikely to exist. The main complication in the development is that the notion of expansiveness does not suffice for a general treatment of the polymorphic let-construct.