|
|
|
|
|
The 2020 MGS Christmas Seminars take place online at 1pm on Tuesday 15 December 2020, and are organised by Leicester, with Birmingham hosting. If you wish to attend please send you email address to Achim Jung at the University of Birmingham. Please note that the seminars will be recorded and made available after the event.
We have four talks, and the speakers are Shin-ya Katsumata, National Institute of Informatics, Japan; Thomas Streicher, University of Darmstadt; Harsh Beohar, University of Sheffield; and Roy Crole, University of Leicester.
If you are new to MGS, you might like to know that the Midlands Graduate School (MGS) provides an intensive course of lectures on the Mathematical Foundations of Computing Science. It has run annually since 1999 and has been held at either the University of Birmingham, the University of Leicester, the University of Nottingham, or at the University of Sheffield. The lectures are aimed at graduate students, typically in their first or second year of study for a PhD. However, the school is open to anyone who is interested in learning more about mathematical computing foundations, and all such applicants are warmly welcomed. We very much encourage learners from abroad and from industry to attend, and many have done so in the past.
The next MGS Graduate School is in April 2021, online, and hosted by Sheffield
| 1300-1345 | Shin-ya Katsumata . National Institute of Informatics, Japan. | |
| 1345-1430 | Thomas Streicher. Darmstadt, Germany. | |
| 1430-1445 | Break | |
| 1445-1530 | Harsh Beohar. Sheffield | |
| 1530-1600 | Roy Crole. Leicester | |
| 1600 | Pub |
Bisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent rise of interest in quantitative systems (probabilistic, weighted, hybrid, etc.), bisimilarity has been extended in various ways: notably, bisimulation metric between probabilistic systems. An important feature of bisimilarity is its game-theoretic characterization, where Spoiler and Duplicator play against each other; extension of bisimilarity games to quantitative settings has been actively pursued too.
In this paper, we present a general framework that uniformly describes game characterizations of bisimilarity-like notions. Our framework is formalized categorically using fibrations and coalgebras. In particular, our characterization of bisimilarity in terms of fibrational predicate transformers allows us to derive codensity bisimilarity games: a general categorical game characterization of bisimilarity.
This is a joint work with Yuichi Komorida, Nick Hu, Bartek Klin and Ichiro Hasuo.
Triposes were introduced in 1980 by Hyland, Johnstone and Pitts as fibered posets P over a topos SS which by adding "subquotients" give rise to a topos SS[P] together with a so called "constant objects" functor Delta_P : SS --> SS[P] embedding the ground model SS into SS[P]. We characterise such functors by a weakening of the requirements for a localic geometric morphism. We also show that nonequivalent triposes over Set may give rise to the same topos.
Our notion of tripos is a bit weaker than the traditional one. We discuss why this weakening is reasonable.
In theory of coalgebras, the framework based on contravariant (dual) adjunction to develop expressive modal logic is already well established. Nevertheless, somehow this framework is difficult to instantiate for coalgebras living in Kleisli categories. In this talk, we build upon the recent work of Kupke and Rot [Expressive Logics for Coinductive Predicates, CSL’20] and develop an expressive logic w.r.t. behavioural equivalence for coalgebras living in concrete categories over the category of sets. We apply this framework to derive expressive logic for nondeterministic automata (conditional transition systems if time permits).
This is part of a joint work with Barbara König, Christina Mika-Michalski, and Sebastian KÜpper.
In first year hardware texts, one finds simple conditions for ALU addition correctness. However, the details are often informal and incomplete. As someone who has taught Computer Architecture for some years, I always found this a little frustrating. While in many ways this is a "trivial" topic, I could never find a clear, simple, precise summary which I could show to students. This led me to write an article, which is simple but fun, and is joint work with Samuel Balco. Here is a little more formal detail:
Mathematical addition of natural numbers, where columns of digits are added up and all carry and output digits computed, is always correct. Addition of natural numbers, performed by an Arithmetic Logic Unit (ALU) in a computer processor, may or may not be correct. We explore operations each of which is a form of addition or subtraction or negation. For each operation, a correctness theorem is proven, where conditions which are either total or conditional, characterise correctness.