We extend Herbelin's sequent calculus for intuitionistic propositional logic by adding dependent types, polymorphism, and type constructors. We thus get eight systems that correspond logically to the corners of Barendregt's Cube.

Proof-search is naturally done in the cut-free fragment, which is somewhat simpler than defining a proof-search strategy in natural deduction to obtain proofs in normal form only. As opposed to Gentzen-style sequent calculi, Herbelin's formalism is a permutation-free sequent calculus, which avoids redundency in proof-search, so that cut-free proofs are in one-to-one correspondence with normal forms of natural deduction. The formalism is actually closer than natural deduction to the representation of proofs in software like Coq, and the proof-search tactics currently implemented in the latter more closely correspond to the typing rules of sequent calculus than those of natural deduction.

Proven theorems are Thinning, Subject Reduction, Confluence, Strong Normalisation...

Conversion rules for types are needed in most of the eight systems, so it is interesting to formalise "syntax-directed" versions where the conversion rules are incorporated in the minimal though necessary places of the other rules. In such versions type inference and proof-search can be optimised.

As sequent calculus is also a neat way of presenting classical logic, we would also like to define a classical version of the above systems, and I will mention some issues about doing so.