LOGICS FOR RESOURCES, PROCESSES, AND PROGRAMS
(in conjunction with IJCAR 2012)
Manchester, UK, 1st July, 2012
A special issue of a Journal on these topics is expected after the workshop.
The notion of resource is a basic one in many fields, but it appears as central in computer science. The location, ownership, access to, distribution of, mobility of, and, indeed, consumption of, resources are central concerns in the design of systems (such as networks and operating systems) and of programs which access memory and manipulate data structures (such as pointers). Various logics, typically involving substructural connectives, have been proposed in order to provide a logical analysis of this notion from different viewpoints. Examples include linear logic (number-of-uses reading), the bunched implications logic (sharing and separating interpretations), so-called separation and spatial logics (pointer logic and local reasoning, logics for concurrency, logics for data structures such as trees). Logics such as these, which may include a wide range of modalities and domain-specific operators, allow the description of properties of systems, of process calculi, and of programs, and so provide bases for specification and theorem-proving tools.
The purpose of this workshop would be to discuss recent results on logics, including systems formulated in the style of Hoare and Hennessy-Milner, for modelling resources, processes, programs, and their interactions. We envisage a range of perspectives: proof-theoretic foundations, including decidability and complexity; semantic foundations (e.g., new resource semantics); specification of properties and behaviours; verification and analysis of programs and systems. It should help to establish and publicize a research agenda for such logics and their use in the development of trusted systems.
The workshop is intended to provide a forum for discussion between researchers interested in logics of resources (from foundations to related calculi and applications) and researchers interested in languages and methods for specification of mobile, distributed, concurrent systems and their verification.
Topics of interest, in this context, include but are not restricted to the following:
Peter O'Hearn (UCL)
Researchers interested in presenting their works are invited to send an extended abstract (up to 10 pages)} by e-mail submissions of PDF files to Didier Galmiche (Didier.Galmiche@loria.fr) and D. Pym (d.j.pym@abdn.ac.uk) before May 15, 2012 . Papers will be reviewed by peers, typically members of the programme committee.
Program Committee