Logic and computation
We present different formal reasoning systems: Hilbert axioms, natural deduction and sequent calculus. We show how each system entails a different programming language: combinatory logic, lambda-calculus and sequent calculus recast as a term calculus. The focus is on classical systems. This leads to programming languages with control operators. Proof transformations are shown to correspond to evaluation mechanisms and compilation techniques. Logic concepts of duality, focalization and polarization are shown to have a computational interpretation.
- Z. Ariola. Logic and computation. Slides from the course at EWSCS '19.
- Videos from the lectures (large, unedited files) [mp4, password-protected]
April 10, 2020 22:41 Europe/Helsinki (GMT +03:00)
local organizers, ewscs19(at)cs.ioc.ee
EWSCS'19 page: //cs.ioc.ee/ewscs/2019/