Re: [TYPES] Looking for concurrent imperative core Java calculi

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Massimo, you may also want to take a look at K-Java, recently presented at POPL'15, which is a complete formal semantics of Java 1.4 (including threads).

Grigore



________________________________________
From: Types-list [types-list-bounces-nHFbR+4dATOoZA3Q9b/[email protected]] on behalf of Massimo Merro [[email protected]]
Sent: Friday, January 23, 2015 3:13 AM
To: Antonio Ravara
Cc: types-list-nHFbR+4dATOoZA3Q9b/[email protected]
Subject: Re: [TYPES] Looking for concurrent imperative core Java calculi

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear Antonio,

we just finisched a paper on semantics for locking specifications in Java. In the paper
you can find a core Java calculus modelling thread-based concurrency and locking semantics.

Semantics for Locking Specifications
Michael Ernst, Damiano Macedonio, Massimo Merro and Fausto Spoto.

Here is a references:

> http://arxiv.org/abs/1501.05338


All the best,
--Massimo


Il giorno Jan 21, 2015, alle ore 1:42 PM, Antonio Ravara ha scritto:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Dear all,
>
> I'm looking for references of works with imperative core Java calculi modelling thread-based concurrency and lock-based synchronisation.
>
> I've found Johan Östlund and Tobias Wrigstad Welterweight Java, but I wonder if there are other and/or more recent works.
>
> Thanks,
> antonio
> --
> Antonio Ravara
>
> Member of NOVA-LINCS (URL: nova-lincs.di.fct.unl.pt/)
> Assistant Professor at Dep. of Informatics, FCT, Univ. NOVA de Lisboa (New University of Lisbon)
> Web page: ctp.di.fct.unl.pt/~aravara/