<div dir="ltr">The only dissertation on the subject that I'm aware of is Lars Åke Fredlund's thesis from 2001: "A Framework for Reasoning about ERLANG Code"<div><br></div><div>It uses modal logic to model time; specifically an extension of the mu-calculus in the "usual" Gentzen-style deductive framework.</div>
<div><br></div><div>If there are other approaches that have been investigated for Erlang specifically, I'd be very interested in links etc!<br><div><br></div></div><div>/// Raphael</div></div><div class="gmail_extra">
<br><br><div class="gmail_quote">On Mon, Jun 23, 2014 at 2:17 PM, Ignas Vyšniauskas <span dir="ltr"><<a href="mailto:i.vysniauskas@gmail.com" target="_blank">i.vysniauskas@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="">On Mon, Jun 23, 2014 at 2:43 PM, Raphael Korsoski <<a href="mailto:psidrinal@gmail.com">psidrinal@gmail.com</a>> wrote:<br>
> I'd go so far as to say that Erlang and the Actor Model are in the same<br>
> programming paradigm, but with different axioms in their semantics--<br>
> although that's of course conjecture without (large, tedious) proof....<br>
><br>
> In my opinion, strictly separating Erlang-style concurrency and the Actor<br>
> model is only of academic interest; unless you are implementing, say, an<br>
> Erlang runtime of course. The differences are certainly relevant to category<br>
> theorists, language theorists, mathematicians working in the Curry-Howard<br>
> domain and so forth, but for the general programmer the differences are more<br>
> or less implementation details ("up-to the usual nonsense").<br>
<br>
</div>I agree with you in the general spirit of "formally it doesn't matter<br>
much because it's mostly the same thing."<br>
<br>
However, there is one crucial thing in Erlang which, on the positive<br>
side makes it a very practical tool, and on the negative side makes it<br>
very hard to talk about formal semantics and prove things like<br>
progress. This is the availability of the `receiver .. after ..`<br>
primitive. Allowing local-timing-based behaviour in processes usually<br>
means that you need some very strong global fairness assumptions in<br>
order to do any kind of formal proofs. I don't see how one could<br>
obtain a (useful) representation of Erlang semantics in any of the<br>
usual process calculi without ignoring this fact. It would be<br>
interesting to find out if anyone ever did something similar formally.<br>
<br>
--<br>
Ignas<br>
</blockquote></div><br></div>