We investigate in the use of constructive logics (e.g. higher-order linear
and intuitionistic logic) as specification languages for computational
systems (e.g. concurrent and sequential systems)
where agents have complex structure (e.g., object-oriented systems).
Being strictly related to the formalism of Petri Nets, linear logic turns
out to be particularly well-suited to model concurrent aspects of
We are exploring this connection to develop automated deduction techniques
for constructive logics based on the algorithms used for the analysis
of Petri Net-like models.