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

Tag: type-checking

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.

My thesis is out!

At last! The definitive, final and comprehensive version of my thesis manuscript is out. I defended it on April 8 in Bologna, Italy, and received both titles of “Dottore di ricerca” and “Docteur” in Computer Science, with great pride and relief. What an adventure! You can find my manuscript on my web page, precisely here; it’s called Certificates for incremental type-checking, and after much hesitation, I chose a blue cover for its printed version (it was a tough choice). It is already a little bit obsolete since I compulsively worked on that material even after its submission to avoid the baby blues, but I will nonetheless advertise it here, and eventually write about my advances in future posts. In short, if you are interested in proof certificates, manipulation of proof objects in a functional language, spine-form LF, incremental type-checking, contextual type theory, or the relationship between natural deduction and the sequent calculus, you might be interested in some parts of my manuscript.

Read the rest of this entry »

Reverse natural deduction and get sequent calculus

This is a follow-up on my previous post. It should be readable by itself if you just take a quick peek at herds.

Today, we are going to write type-checkers. And rewrite them. Again and again. Eventually, I’ll put in evidence that what seemed to be a programming hack in the last post turns out to be the difference between two well-known equivalent formulations of first-order logic, your good ol’ natural deduction and sequent calculus. Read the rest of this entry »

Building terms, incrementally

Here is the first post of a series about incremental verification in programming languages. This problem has become more-or-less the main subject of my Ph.D, and this is an exercise in explaining it from scratch, exploring all the possible alternatives.

Eventually, the goal is to have a clear foundation for supporting better typing incrementality in programming and proof development tools. By incrementality, I mean the ability to have feedback of type errors upon any change during the development. This requires the ability to check changes in programs or proofs and not have to retype a whole development or file as it is the case too often. Read the rest of this entry »