What We Do
Our work concerns the development and study of precise mathematical formalisms that can be employed for the design, specification, and verification of computer programs. This is in a tradition of mathematical semantics that was started in the UK in the 1960s by Peter Landin, Christopher Strachey, and Dana Scott. This kind of semantics encompasses many mathematical theories, foremost among them order theory, topology, logic, game theory, and category theory, all of which feature in the work of the Birmingham Theory Group. It is the rich and often surprising interplay between these mathematical areas and programming concerns that gives rise to opportunities for deep and profound research.
Recent work has included the following topics:
- linear logic and continuation semantics: Berdine, O'Hearn, Reddy, Thielecke: Linear Continuation Passing. Higher Order and Symbolic Computation, vol. 15, pages 181-208, 2002.
- verification of concurrent imperative programs: Reddy, Reynolds: Syntactic Control of Interference for Separation Logic. ACM Symp. on Principles of Programming Languages, 2012.
- compilation of functional programs into hardware: Ghica, Smith: Geometry of Synthesis III: Resource management through type inference. 38th Symposium on Principles of Programming Languages, 2011.
- application of process calculi to security: Arapinis, Chothia, Ritter and Ryan: Analysing Unlinkability and Anonymity Using the Applied Pi Calculus. Computer Security Foundations Symposium 2010 (CSF'10), pp. 107-121.
- extensions to Stone duality: Jung, Moshier: On the bitopological nature of Stone Duality. Technical Report CSR-06-13. School of Computer Science, University of Birmingham, 2006, 110 pages.
- applications of geometric logic to topos approaches to quantum theory: Fauser, Raynaud, Vickers: The Born rule as structure of spectral bundles. 8th International Workshop on Quantum Physics and Logic, 2011.
- direct topological arguments for proving higher-order programs correct: Escardo, Ho: Operational domain theory and topology of a sequential programming language. 20th Annual IEEE Symposium on Logic in Computer Science, 2005.
- universal constructions on monads: Bowler, Goncharov, Levy, Schröder: Exploring the boundaries of monad tensorability on Set. Logical Methods in Computer Science 9(3), 2013.
- the relationship between temporal logic and interactive programming: Krishnaswami: Higher-Order Reactive Programming without Spacetime Leaks. 18th ACM SIGPLAN International Conference on Functional Programming, 2013.
One of the most fascinating aspects of our work is that the mathematical theories we explore have found interest and application beyond the realm of semantics. A prime example of this is the link between type theory and homotopy theory which shows promise to provide a new constructive foundation for mathematics. Similarly, work in abstract category theory, originally developed with applications in computing in mind, is now being deployed for a new foundation of quantum physics.
Members of the Birmingham Theory Group have written many of the widely-cited fundamental texts that expound the core techniques and principles of mathematical semantics, for example
- Samson Abramsky and Achim Jung: Domain Theory. In Handbook of Logic in Computer Science, vol. III, Clarendon Press, 1994, pages 1-168.
- Steve Vickers: Topology via Logic. Cambridge Tracts in Theoretical Computer Science, vol. 5, Cambridge University Press, 1989.
- Martin Escardo: Synthetic topology of data types and classical spaces. In Domain-theoretic Methods in Probabilistic Processes, vol. 87, Electronic Notes in Theoretical Computer Science, 2004.
- Paul Levy: Call-by-push-value. A functional/imperative synthesis. Semantic Structures in Computation, Springer 2004.
- Uday Reddy: Global state considered unnecessary: An introduction to object-based semantics. Journal on Lisp and Symbolic Computation vol. 9, 1996, pages 7-76.
- David Pym and Eike Ritter: Reductive Logic and Proof-search: Proof Theory, Semantics, and Control. Oxford Logic Guides, Oxford University Press, 2004.
We are co-founders of the Midlands Graduate School in the Foundations of Computing Science which has introduced more than 400 PhD students and researchers to foundational and advanced topics in mathematical semantics, and have participated in many similar events worldwide.
The Group runs twice-weekly lab sessions and a weekly seminar series with speakers from the UK and beyond.