f(by) 2019, Alex Gryzlov - LOGIC, MACHINES AND SEQUENT CALCULUS

Have you ever wondered if the foundations of FP could be redesigned from the ground up? In this talk we'll use a logical framework called "sequent calculus" to define an alternative system to the lambda calculus and see the benefits this will bring us, demystifying continuations in the process.

Sequent calculus is a logical formalism invented in 1930s with the aim of analyzing the construction of mathematical proofs. It turns out that applying it to programming gives us a certain "assembly language for FP" that reveals various symmetries of computation: producing/consuming, values/contexts, strictness/laziness and so forth. This computational version of sequent calculus is known under several names in academia, one of them being "system L". In the talk a functional dependently typed language Idris will be used to implement a toy version of system L and prove some of its properties.

Slides: