@inproceedings(CurienHerbelinICFP00,
 author       = {P.-L. Curien and H. Herbelin},
 year         = {2000},
 title        = {The duality of computation},
 booktitle    = {Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, September 18-21, 2000},
 series       = {SIGPLAN Notices 35(9)},
 publisher    = {ACM},
 pages        = {233--243},
 doi          = {10.1145/351240.351262},
)
@book(Prawitz65,
 author       = {D. Prawitz},
 year         = {1965},
 title        = {Natural Deduction. A Proof-Theoretical Study},
 publisher    = {Almquist and Wiksell, Stockholm},
)
@inproceedings(RehofSorensen94,
 author       = {N. Rehof and M. Sorensen},
 year         = {1994},
 title        = {The $\lambda_{\Delta}$-calculus},
 booktitle    = {TACS'94},
 series       = {Lecture Notes in Computer Science},
 volume       = {789},
 publisher    = {Springer Verlag},
 pages        = {516--542},
 doi          = {10.1007/3-540-57887-0\_113},
)
@article(Stalmarck91,
 author       = {G. Stalmarck},
 year         = {1991},
 title        = {Normalization theorems for full first order classical natural deduction},
 journal      = {The Journal of Symbolic Logic},
 volume       = {56},
 number       = {1},
 pages        = {129--149},
 doi          = {10.2307/2274910},
)
@phdthesis(StatmanPhD74,
 author       = {R. Statman},
 year         = {1974},
 title        = {Structural complexity of proofs},
 school       = {Stanford University},
)