Many concepts of computing science can be illustrated in ways that do not require programming. For example, "CS Unplugged" is a well-known resource for that purpose. However, the illustrations in "CS Unplugged" and elsewhere focus on topics such as algorithmics, cryptography, logic and data representation, to the neglect of topics in programming language foundations, such as semantics and type theory.
This paper begins to redress the balance by illustrating the principles of static type systems in two non-programming scenarios where there are physical constraints on forming connections between components. The first scenario involves serial cables and the ways in which they can be connected. The second example involves model railway layouts and the ways in which they can be constructed from individual pieces of track.
In both cases, the physical constraints can be viewed as a type system, such that typable systems satisfy desirable semantic properties.
23/10/2019 13:00
Software Systems
Simon Gay is a Professor of Computing Science at the University of Glasgow, Scotland. Until last month he was Director of Research and head of the Formal Analysis, Theory and Algorithms research section. Now he is on sabbatical before becoming Head of School next year. His main research topic is session types, which are type-theoretic specifications of communication protocols.
