Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell

Gentzen’s Hauptsatz – cut elimination theorem – in sequent calculi reveals a fundamental property on logic connectives in various logics such as classical logic and intuitionistic logic. In this paper, we implement a procedure in Haskell to perform cut elimination for intuitionistic sequent calculus, where we use types to guarantee that the procedure can only return a cut-free proof of the same sequent when given a proof of a sequent that may contain cuts. The contribution of the paper is two-fold. On the one hand, we present an interesting (and somewhat unexpected) application of the current type system of Haskell, illustrating through a concrete example how some typical use of dependent types can be simulated in Haskell. On the other hand, we identify several problematic issues with such a simulation technique and then suggest some approaches to addressing these issues in Haskell.

• Type: Conference
• Year: 2004
• Where: PADL
• Authors: Chiyan Chen, Dengping Zhu, Hongwei Xi
• Keywords: Cut Elimination, Intuitionistic Sequent Calculus, PADL 2004, Programming Languages, Sequent