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

Thank you for visiting! Please consider filling out our questionnaire. This will help us improve our service providing free educational media recorded from the University of Oxford. Many thanks!

Click here to access the survey (3 minutes to complete).

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: