Type Inference for M3 Mobile Ambients
This page demonstrates a prototypal implementation
of a type system for the ambient calculs M3
[Coppo, Dezani-Ciancaglini, Giovannetti, Salvo, 2003].
The current version
(released in October 2003, developed by E. Giovannetti):
implements the algorithm described in
(revised and improved version of
[Coppo, Giovannetti, 2003]);
is written in
accepts as input a raw (i.e., untyped) M3 term,
and returns the principal typing, if it exists, for that term.
Type a term, terminated by a semicolon, in the field below, then press the button.
Here you can find
a description of the accepted
that you can copy and paste.
Coppo, Dezani-Ciancaglini, Giovannetti, Salvo, 2003]
M. Coppo, M. Dezani-Ciancaglini, E. Giovannetti, and I. Salvo.
M3: Mobility types for mobile processes in mobile ambients.
In CATS 2003, volume 78 of ENTCS, 2003.
Coppo, Giovannetti, 2003]
M. Coppo and E. Giovannetti.
Prolog implementation of type inference algorithms for mobile ambients.
Internal report, June 2003.
Type Inference for Mobile Ambients in Prolog.
In CATS 2004, ENTCS, 2004