Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
@inproceedings{CUTELIMpadl04, author = "Chiyan Chen and Dengping Zhu and Hongwei Xi", title = {{Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell}}, booktitle = "Proceedings of the 6th International Symposium on Practical Aspects of Declarative Languages", publisher = "Springer-Verlag LNCS vol. 3057", year = "2004", month = "June", pages = "239--254", address = "Dallas, TX", abstract = {{ 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. }} }