Last updated on 8th December 2017
In addition to its yearly programme of taught courses on the
mathematical foundations of
computing, the Midlands Graduate School holds an afternoon of Christmas Seminars.
The seminars are free, open to everyone, and no registration is required.
14.00 - 15.00:
CALF: A Categorical Automata Learning Framework
Alexandra Silva, University College London
Automata learning is a technique that has successfully been applied in verification, with the automaton type varying depending on the application domain. Adaptations of automata learning algorithms for increasingly complex types of automata have to be developed from scratch because there was no abstract theory offering guidelines. This makes it hard to devise such algorithms, and it obscures their correctness proofs. We introduce a simple category-theoretic formalism that provides an appropriately abstract foundation for studying automata learning. Furthermore, our framework establishes formal relations between algorithms for learning, testing, and minimization. We illustrate its generality with two examples: deterministic and weighted automata.
15.00 - 15.30:
15.30 - 16.15:
Weak Enrichment and Cofibrant Operads
Paolo Capriotti, University of Nottingham
I will talk about the idea of weak enrichment, introduced independently by Todd Trimble and Peter May, and show how it can be used to produce homotopy-coherent definitions of higher categories that are suitable for formalisation in type theory.
16.15 - 17.00:
Generalised Kripke Semantics for Concurrent Quantales
Georg Struth, University of Sheffield
I will present ongoing work on a new technique for constructing models of concurrent quantales (and concurrent Kleene algebras). It is inspired by modal correspondence theory for substructural logics. Frame conditions are given by ternary relations. The operations of concurrent quantales arise as binary modalities---in fact as convolution operations---over quantale-valued functions, parametrised by the ternary frames. The main result is a correspondence theorem between concurrent quantales and frame conditions. A first example constructs concurrent quantales and Kleene algebras of weighted shuffle languages from word-level concatenation and shuffle operations. The second one obtains concurrent quantales of graphs (or graph types) by lifting from the operations of complete join and disjoint union on individual graphs. The concurrent quantales of pomset languages arise as a special case. Similar constructions in separation logic or interval temporal logics illustrate the universality of the approach, if time permits.
(Joint work with James Cranch and Simon Doherty.)
Afterwards we will retire to the pub and then for an early dinner at Kayal in the city centre
for anyone who would like to join us.
Lecture Theatre A25
Business School South Building
Jubilee Campus, University of Nottingham
Wollaton Road, Nottingham NG8 1BB
A map of the Jubilee Campus is available here. The seminars will be in room A25 of the Business School South Building (labelled 7 on the campus map). If you arrive early we suggest participants meet at Spokes Cafe in the Jubilee Conference Centre (labelled 50 on the campus map).
By train or bus: The Jubilee Campus is around 10 minutes by taxi from the train and bus stations in Nottingham city centre.
By car: Enter the Jubilee Campus via the main entrance on Wollaton Road, as the other entrance (on Triumph Road) is only accessible with an electronic pass. Tell the security staff at the main entrance that you are a visitor, and they will direct you to the pay-and-display visitors car park nearby. Make sure not to park elsewhere, as all other spaces require a parking permit and are subject to clamping.
In case you require a taxi as part of your journey, here are some local numbers:
Cable Cars: 0115 922 9229 Central Taxi: 0115 976 2222 County Taxi: 0115 942 5425 DG Taxi: 0115 960 7607