The seminar will take place in room CW408 in the Cathedral Wing Building (G4 0QU) on the University of Strathclyde campus.
| Time (BST) | Wednesday 7 October | Details |
|---|---|---|
| 12:00(noon)–13:00 | Arrival and Lunch | Location: in front of CW408 |
| 13:00–13:45 | Juliana Bowles | From logics and formal models to applications and back I will describe some of the work that I have done over the years on logics, models and reasoning sometimes to solve problems in healthcare, or conversely be inspired by concrete problems to enrich formalisations, etc |
| 13:45–14:30 | Jonni Virtema |
Logics for the specification of hyperproperties Since the 1980s, model checking has become a staple in verification. For Linear Temporal Logic (LTL) and its progeny, the model checking problem asks whether every trace of a given system fulfils a given temporal specification such as a liveness or fairness property. Notably, this specification considers the traces of the input in isolation and cannot relate different traces to each other. However, it is not hard to come up with natural properties that require viewing different traces in tandem. A textbook example is bounded termination; one cannot decide whether a system terminates in bounded time by considering computation traces of the system in isolation. Further typical properties of this kind are many information-flow properties of systems such as observational determinism or generalised non-interference. A common term coined for properties of the aforementioned kind are hyperproperties (in contrast to trace properties). Hyperproperties describe properties of sets of traces, and since LTL and other traditional temporal logics can only specify trace properties, new logics have needed to be designed to fill this gap. In this talk, I review two approaches for designing logics for hyperproperties: a) HyperLTL and is progeny that are obtained from classical temporal logics by extending their syntax with quantifiers ranging over traces, b) TeamLTL and its variants, which adopt team semantics and lift the satisfaction of LTL formulae to sets of traces directly. In addition to introducing these logical formalism, I will review their expressive power (in relation to each other) and the complexity of their model checking and satisfiability problems. |
| 14:30–15:00 | Coffee | Location: in front of CW408 |
| 15:00–15:45 | Robert Atkey |
Data types with Negation Inductive data types are a foundational tool for representing data and reasoning in dependently typed programming languages. The user defines an inductive data type by declaring ways of constructing positive evidence. For example, evidence of a path through some graph, or the existence of a well-typed term, or the parse tree as evidence that a context-free grammar accepts some input. But in some cases positive evidence is not enough. What if we want evidence that no path exists? or we want to represent parse trees of backtracking parsers, where alternatives are only tried in the case when another parse didn’t work? In this talk, I will explain how the use of negative evidence arises in the study of programming languages, describe a way of extending inductive data types with negation, and how we can understand them as an interaction of inductive and coinductive types. |
| 15:45–17:00 | Panel discussion and Planning | Topic: Our aims and plans for future meetings! |
| 17:00–?? | Pub | Location TBD |