ACTIVITIES:

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 computations. 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.