Lambda the Ultimate

Transactions are a hot topic in programming languages, especially with some exciting recent work on providing language support for STM ("Software Transaction Memory"). A new paper, A Concurrent Calculus with Atomic Transactions, by Acciai, Boreale & Dal Zilio, provides an extension of CCS, which they call ATCCS ("Atomic Transactions CCS"), with support for the primary operations of STM.

I was not aware of work on modelling transactions in process calculi, but the bibliography cites six works, five from the last three years, and a Montanari&co paper from 1990:

• 6. L. Bocchi, C. Laneve and G. Zavattaro. A Calculus for Long Running Transactions. In Proc. of FMOODS, LNCS 2884, 2003.

• 8. R. Bruni, H.C. Melgratti and U. Montanari. Nested Commits for Mobile Calculi: extending Join. In Proc. of IFIP TCS, 563-576, 2004.

• 9. R. Bruni, H.C. Melgratti and U. Montanari. Theoretical Foundations for Compensations in Flow Composition Languages. In Proc. of POPL, ACM Press, 209-220, 2005.

• 15. V. Danos and J. Krivine. Reversible Communicating System. In Proc. of CONCUR, LNCS 3170, 2004.

• 16. V. Danos and J. Krivine. Transactions in RCCS. In Proc. of CONCUR, LNCS 3653, 2005.

• 18. R. Gorrieri, S. Marchetti and U. Montanari. ACCS: Atomic
  Actions for CCS. Theoretical Computer Science,
  72(2-3):203-223, 1990.

I haven't read these papers, but from the summary in the concluding paper of the ABZ paper, there seem to be some interesting ideas floating about here. Will repay a closer look, I think...

Hi,

Please be gentle with me, this is my first post :-)

I am currently writing my master thesis (CS) on the topic of adding type inference to the formal specification language VDM++.

VDM++ is an object-oriented, formal specification language, typically used to model mission-critical systems. The syntax is mathematically oriented, using a lot of abstract constructs such as sets, sequences, maps and unions as well as more widespread language constructs.

If anyone is interested in the language spec, it can be found here:
http://www.vdmbook.com/langmanpp_a4.pdf

Anyway, to my question...
I am looking for some pointers to literature on the use of union types, specifically the problems which union types may cause in connection with type inference. In VDM++, unions correspond to set-theoretic unions of two or more types which may be disjoint or non-disjoint.

There seems to be plenty written on intersection types, but union types and ways to statically handle these seem quite scarce.

Bjarne Stroustrup. A rationale for semantically enhanced library languages. LCSD05. October 2005.

This paper presents the rationale for a novel approach to providing expressive, teachable, maintainable, and cost-effective special-purpose languages: A Semantically Enhanced Library Language (a SEL language or a SELL) is a dialect created by supersetting a language using a library and then subsetting the result using a tool that “understands” the syntax and semantics of both the underlying language and the library.

How similar or different this idea really is compared to the facilities found in PLT Scheme and other previous apporaches to this issue?