Résumé:
The talk will cover the design of a small step operational semantics
for a subset of the Erlang programming language. Erlang combines an
interesting mix of programming styles: functional in the large, with
call-by-value semantics, and with prominent support for concurrency
and communication through the explicit introduction of processes and
message passing. The developed semantics is a hierarchic one, in
order to cleanly separate these concerns.
The point of the presented work is not to create an authoritative
definition of the Erlang language - the language is to a very large
degree defined by its implementations. The emphasis is rather on
providing a semantics that is practically useful for reasoning about
Erlang programs, or classes of Erlang programs, by means of a proof
system, and supported in a proof assistant tool.
The talk will very briefly summarise also the overall
work on the proof system for Erlang, and its implementation.
Retour au sommaire / Back to schedule