Sequent calculus cheat sheet
Rules for sequent calculus connectives, formatted as a cheat sheet.
When Howard Met Curry
The Curry-Howard correspondence is a map for moving between logic and type theory, relating propositions with types and proofs with programs. It describes a two-way street, and we can freely move between the two worlds, or perhaps merely two perspectives, so long as we follow the map.
Sometimes the road takes us to unexpected places. Here’s a trip I’ve been on recently.
Sequent Calculi and Metacircularity
Sequent calculi are powerful and flexible tools for studying logic and, via Curry-Howard, computation. But why, and how? Where does this power come from?
Environment-Passing Style
Functions of type A → B can be translated into corresponding functions of type ¬B → ¬A in continuation-passing style (CPS), where ¬A is logically negation but computationally a continuation from A.
Duality
The rules for a variety of polarized classical connectives, in a focused sequent calculus presentation to reflect a variety of dualities, and interpreted via Curry-Howard.
All you need is λ, part one: booleans
Nearly a century ago, Alonzo Church invented the simple, elegant, and yet elusive lambda calculus. Along with Alan Turing, he then proved the Church-Turing thesis: that anything computable with a Turing machine can also be computed in the lambda calculus. However, nearly as soon as we had digital computers, we started inventing programming languages, and with them a vast treasure of features, beautiful and terrible, many of which seem very hard to relate to the fundamental nature of computability, let alone the lambda calculus specifically.
Pattern matching over recursive values in Swift
Swift’s value types are almost able to represent algebraic data types. Unfortunately, they fall short of the mark when it comes to recursion, and while they’ve announced that their solution, indirect cases, will ship in a later build of Swift 2, there’s still reason to want them today.