### Sequent calculus cheat sheet

Aug 14, 2021, 7:01 PM

Rules for sequent calculus connectives, formatted as a cheat sheet.
Additive
Multiplicative
Implicative
Negation
Assertion
Shifts
Quantification
Core
Structural
...

### 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...

### Environment-Passing Style

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...

### Duality

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.
Additive
1
...

### 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ⁿ...