Logic, Machines and Sequent Calculus

Code for the talk.

2019 Version: https://www.youtube.com/watch?v=O0TgP7GKkSY

2018 Version: https://www.youtube.com/watch?v=9l6FD9gRGxc

Modules by their appearance:

• List - some properties of lists
• Lambda - untyped lambda calculus
• STLC - simply-typed lambda calculus
• SC - one-sided sequent calculus LJ
• LK - two-sided core sequent calculus LK
• LKConn - LK with additional connectives
• LKLamApp - LK and deconstruction of lambdas
• KAM - Krivine abstract machine for untyped lambda
• CEK - Control+Environment+Kontinuation abstract machine for untyped lambda
• LKT - focused call-by-name version of LK
• LKQ - focused call-by-value version of LK

References

• Kokke, "One lambda-calculus, many times"
• Downen, Ariola, "A Tutorial on Computational Classical Logic and the Sequent Calculus"
• Spiwack, "A dissection of L"
• Maillard et al, "A preview of a tutorial on polarised L calculi"
• Munch-Maccagnoni, "Syntax and Models of a non-Associative Composition of Programs and Proofs"