Mon 26 Oct 2015 14:10 - 14:30 at Grand Station 4 - Session 3 - Types and Verification

The two main characteristics of the Actor model are asynchronous message passing and dynamic system topology. The latter relies on the on-the-fly creation of actor names that often complicates the formal treatment of systems described in the Actor model. In this paper, we introduce Actario, a formalization of the Actor model in Coq. Actario incorporates a name creation mechanism that is formally proven to generate a consistent set of actor names. The mechanism helps proper handling of names in modeling and reasoning about actor-based systems. Actario also provides a code extraction mechanism that generates Erlang programs.

Mon 26 Oct
Times are displayed in time zone: (GMT-04:00) Eastern Time (US & Canada) change

13:30 - 15:00: AGERE - Session 3 - Types and Verification at Grand Station 4
agere201513:30 - 13:50
Sylvan ClebschImperial College London, Sophia DrossopoulouImperial College London
Media Attached
agere201513:50 - 14:10
Stefan MarrINRIA, France, Hanspeter MössenböckJohannes Kepler University Linz
Link to publication Pre-print Media Attached
agere201514:10 - 14:30
Shohei YasutakeTokyo Institute of Technology, Takuo WatanabeTokyo Institute of Technology
Link to publication Pre-print Media Attached
agere201514:30 - 14:50
Najah Ben SaidVerimag, Takoua AbdellatifUniversity of Sousse, Saddek BensalemVerimag, Marius BozgaVerimag/CNRS