A research blog about programming languages, formal logics, software development and their interactions, by Matthias Puech.

Tag: CPS

Escaping continuations

Beta had a funny joke at POPL last year; he said: “you exit a monad like you exit a building on fire: by running”. I recently got myself in the stressful situation of being trapped in a monad—the continuation monad—but without a possibility to “run”. There an exit nonetheless: just jump out! This is the (short) story of an escape.

Read the rest of this entry »

Update on Typeful Normalization by Evaluation

In October, I publicized here a new draft on normalization by evaluation, which provoked some very helpful comments and constructive criticisms. Together with Chantal and Olivier, we thus revised the draft profoundly and a revamped version is available on my web site.

Besides the enhanced form and better explanations, we included a completely new section on what it means for NbE to be written in Continuation-Passing Style, that I am particularly excited about. This allowed us to extend our typeful NbE formalization beyond the minimal λ-calculus to sums and call/cc (which is known to be difficult). Taking our code, you can write a program with call/cc and if statements, and partially evaluate it: all redexes will be removed and your code will be specialized. All this, as before, is done typefully, thanks to OCaml’s GADTs: this means that the transformation is guaranteed to map well-typed terms to well-typed normal forms.

Read the rest of this entry »

New draft: Proofs, upside down

There is a new draft on my web page, that should be of interest to those who enjoyed my posts about reversing data structures and the relation between natural deduction and sequent calculus. It is an article submitted to APLAS 2013, and it is called Proofs, upside down. In a nutshell, I am arguing for the use of functional PL tools, in particular classic functional program transformations, to understand and explain proof theory phenomena. Here, I show that there is the same relationship between natural deduction and (a restriction of) the sequent calculus than between this recursive function:

let rec tower_rec = function
  | [] -> 1
  | x :: xs -> x ∗∗ tower_rec xs

let tower xs = tower_rec xs

written in “direct style”, and that equivalent, iterative version:

let rec tower_acc acc = function
  | [] -> acc
  | x :: xs -> tower_acc (x ∗∗ acc) xs

let tower xs = tower_acc 1 (List.rev xs)

written in “accumulator-passing style”. And that relationship is the composition of CPS-transformation, defunctionalization and reforestation, the well-known transformations we all came to know and love!

I hope you enjoy it. Of course, any comment will be much appreciated, so don’t hesitate to drop a line below!

Proofs, upside down
A functional correspondence between natural deduction and the sequent calculus
It is well-known in proof theory that sequent calculus proofs differ from natural deduction proofs by “reversing” elimination rules upside down into left introduction rules. It is also well-known that to each recursive, functional program corresponds an equivalent iterative, accumulator-passing program, where the accumulator stores the continuation of the iteration, in “reversed” order. Here, we compose these remarks and show that a restriction of the intuitionistic sequent calculus, LJT, is exactly an accumulator-passing version of intuitionistic natural deduction NJ. More precisely, we obtain this correspondence by applying a series of off-the-shelf program transformations à la Danvy et al. on a type checker for the bidirectional λ-calculus, and get a type checker for the λ-calculus, the proof term assignment of LJT. This functional correspondence revisits the relationship between natural deduction and the sequent calculus by systematically deriving the rules of the latter from the former, and allows to derive new sequent calculus rules from the introduction and elimination rules of new logical connectives.