Over 4000 free audio and video lectures, seminars and teaching resources from Oxford University.
Skip to Content Skip to Navigation

How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation

Loading Video...
Duration: 0:16:55 | Added: 18 Dec 2017
Makoto Hamana (Gunma University, Japan), gives the first talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP conference.

We present a general methodology of proving decidability of equational theory of programming language concepts in the framework of second-order algebraic theories of Fiore, Hur and Mahmoud. We propose a Haskell-based analysis tool SOL, Second-Order Laboratory, which assists the proofs of confluence and strong normalisation of computation rules derived from second-order algebraic theories.

To cover various examples in programming language theory, we combine and extend both syntactical and semantical results of second-order computation in non-trivial manner. In particular, our choice of Yokoyama's deterministic second-order patters as a syntactic construct of rules is important to cover a wide range of examples, such as Hasegawa's linear lmd-calculus. We demonstrate how to prove decidability of various algebraic theories in the literature. It includes the equational theories of monad and computational lmd-calculi, Staton's theory of reading and writing bits, Plotkin and Power's theory of states, and Stark's theory of pi-calculus.

Copy and paste this HTML snippet to embed the audio or video on your site: