Oliver Scarlet

Working with type systems and communications can be very difficult. In Haskell, messages between threads are usually conveyed through channels that only accept a single type, and as a result are not very versatile. In networked systems, a stream of bytes is sent that hopefully conforms to one of many protocols including TCP, UDP, and HTTP, and hopefully both parties agree on what is sent and when. Session Types are a way to bridge the gap between these systems, as they can capture complicated protocols, and be properly type checked. There are many ways that Session Types are notated and…

At Matrix AI our research into language constructs for formally describing distributed systems has led us to a concept called Linear Temporal Logic. It is a logic system that allows us to express logical statements about time. This article will provide a brief introduction to this logic system. Linear Temporal Logic takes the basic ideas of Propositional and Predicate logic and introduces concepts about time. Predicate logic is widely used for automatically checking and proving theorems, verifying software correctness and security, and is the foundation of the programming language ProLog. In Linear Temporal Logic (LTL), we can express statements about…