|
Chiyan Chen, Dengping Zhu, and Hongwei Xi
Implementing cut
elimination: A case study of simulating dependent types in
Haskell
In Proceedings of the 6th International Symposium on Practical
Aspects of Declarative Languages, pages 239-254, Dallas, TX, June 2004
Springer-Verlag LNCS vol. 3057
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.
[ bib |
.ps |
.pdf ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all persons copying this information will
adhere to the terms and constraints invoked by each author's
copyright. These works
may not be reposted without the explicit permission of the copyright
holder.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
|
