Sequent calculus cheat sheet
Aug 14, 2021, 7:01 PM
Rules for sequent calculus connectives, formatted as a cheat sheet.
When Howard Met Curry
Jul 28, 2021, 4:31 PM
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...
Sequent Calculi and Metacircularity
Jul 16, 2021, 12:06 PM
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?
We enjoy a variety of idioms to describe the relationship between problems and...
Jul 8, 2021, 6:08 AM
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.
This widens the view of functions as...
Jun 7, 2021, 3:49 PM
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
Mar 29, 2020, 4:17 PM
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...
Pattern matching over recursive values in Swift
Jun 30, 2015, 10:29 PM
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...
On the Order of Neptune
Apr 20, 2014, 12:20 AM
Inscribe the orbit of Neptune in a square.
Now, take a pair of integers as x and y coordinates across this square. Their size in bits determines the resolution at which they can measure this square.
An integer of n bits can hold any of 2ⁿ...