Skip to main content
Home

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

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

Series
International Conference on Functional Programming 2017
Video Embed
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.

More in this series

View Series
International Conference on Functional Programming 2017

Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols

Geoffrey Mainland (Drexel University, USA) gives the fourth talk in the first panel, Low-level and Systems Programming, on the 2nd day of the ICFP conference.
Previous
International Conference on Functional Programming 2017

Foundations of Strong Call by Need

Thibaut Balabonski (LRI, France and University of Paris-Sud, France) gives the third talk in the second panel, Foundations of Higher-Order Programming, on the 2nd day of the ICFP conference.
Next
Licence
Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series
International Conference on Functional Programming 2017
People
Makoto Hamana
Keywords
technology
computing
programming
Department: Department of Computer Science
Date Added: 18/12/2017
Duration: 00:16:55

Subscribe

Apple Podcast Video Video RSS Feed

Download

Download Video

Footer

  • About
  • Accessibility
  • Contribute
  • Copyright
  • Contact
  • Privacy
'Oxford Podcasts' Twitter Account @oxfordpodcasts | MediaPub Publishing Portal for Oxford Podcast Contributors | Upcoming Talks in Oxford | © 2011-2022 The University of Oxford