Matteo Acclavio visiting Swansea

Next week's theory seminar will be given by Matteo Acclavio from the University of Sussex, who is visiting us for a few days. The topic will be a new logical framework for concurrent programs, abstract below.

Title: A new logical framework for concurrent programs

Abstract:
Designing logical frameworks to reason about the properties of concurrent programs while accurately capturing the essence of concurrency is a challenging task.
The main difficulties can be traced back to the syntactic constraints of the languages used for this purpose.

In this talk, I will present my ongoing line of research, which aims to provide a new computation-as-deduction paradigm for the study of concurrent programs.
In particular, I will show you a non-commutative logic where we can interpret proofs as computation trees for the pi-calculus, and use proof nets to provide canonical representations of these trees modulo interleaving concurrency.

This work is based on joint works with Giulia Manara and Fabrizio Montesi

Next week's Theory Seminar Series

Next week Troy will give a talk on Conceptualising Programming Language Semantics as a part of our seminar series.

Abstract:

Research on the semantics of programming language has tended towards formalisation. Following the successful deployment and myriad uses of formal syntax, many of those working on semantics assumed similar successes would be realised with formal semantics. 

The reality was different, and the resultant language specifications were large, complicated, technical artefacts. My previous historical research has studied those from a technical perspective. 

In this talk, I will explore the conceptual surroundings of the semantics, examining the use of metaphors, analogies, and illustrative language used to accompany or explain the formal documents.

It is early stage research and will focus primarily on picking examples from the history of semantics for deeper analysis in the future.

I will also present some philosophical frameworks I am considering for use in this analysis and begin to discuss how they might help us understand the topic.

This research will ultimately lead to a conference presentation and journal article next year, as well as forming a pilot study for a research grant proposal.

Galileo Sartor's talk

Today's theory seminar talk will be by Galileo Sartor on "Representing and reasoning with legal aspects of traffic rules for autonomous vehicles". 

Abstract:

In this talk, I will give an overview of a modular system for representing and reasoning with legal aspects of traffic rules for autonomous vehicles.
We focus on a subset of the United Kingdom's Highway Code (HC) related to junctions.
As human drivers and automated vehicles (AVs) will interact on the roads, especially in urban environments, we claim that an accessible, unitary, high-level computational model should exist and be applicable to both users.
Autonomous vehicles introduce a shift in liability that should not bring disadvantages or increased burden on human drivers.
The proposed system is built of three main components: a natural language interface, using Logical English, used to encode the rules; an internal representation of the rules in Prolog; and a simple multi-agent-based simulation environment, built in NetLogo. The three components interact: Logical English is internally translated in Prolog, and the resulting code (along with some support code) interfaces with NetLogo with a bridge.
Such a modular approach enables the different components to carry different ``burdens'' in the overall system; it also allows replacing modules.
With the NetLogo simulation, we can visualize the effect of the modeled rules as well as validate the system with a simple dynamic running scenario.
Designated agents monitor the behaviour of the vehicles for compliance and record potential violations where they occur. The information on potential violations is then utilized by validator agents, to determine whether the violation is punishable, differentiating between exceptions and cases.