@inproceedings(artemov_jonghs_2004,
 author       = {Sergei~N. Artemov and Rosalie Iemhoff},
 year         = {2004},
 title        = {From de {Jongh}'s theorem to intuitionistic logic of proofs},
 booktitle    = {Dick de Jongh's Festschrift},
 pages        = {1--10},
 url          = {https://istina.msu.ru/publications/article/19375470/},
)
@book(girard_proofs_1989,
 author       = {Jean-Yves Girard and Paul Taylor and Yves Lafont},
 year         = {1989},
 title        = {Proofs and types},
 series       = {Cambridge tracts in theoretical computer science},
 volume       = {7},
 publisher    = {Cambridge University Press},
 address      = {Cambridge},
 url          = {http://www.paultaylor.eu/stable/prot.pdf},
)
@article(godel_uber_1958,
 author       = {Kurt G\"odel},
 year         = {1958},
 title        = {\"Uber eine bisher noch nicht benützte {Erweiterung} des finiten {Standpunktes}},
 journal      = {Dialectica},
 volume       = {12},
 number       = {3-4},
 pages        = {280--287},
 doi          = {10.1111/j.1746-8361.1958.tb01464.x},
)
@article(harrop_disjunctions_1956,
 author       = {Ronald Harrop},
 year         = {1956},
 title        = {On disjunctions and existential statements in intuitionistic systems of logic},
 journal      = {Mathematische Annalen},
 volume       = {132},
 number       = {4},
 pages        = {347--361},
 doi          = {10.1007/BF01360048},
)
@article(iemhoff_nother_2001,
 author       = {Rosalie Iemhoff},
 year         = {2001},
 title        = {A(nother) characterization of intuitionistic propositional logic},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {113},
 number       = {1},
 pages        = {161--173},
 doi          = {10.1016/S0168-0072(01)00056-2},
)
@article(iemhoff_admissible_2001,
 author       = {Rosalie Iemhoff},
 year         = {2001},
 title        = {On the admissible rules of intuitionistic propositional logic},
 journal      = {The Journal of Symbolic Logic},
 volume       = {66},
 number       = {1},
 pages        = {281--294},
 doi          = {10.2307/2694922},
)
@article(iemhoff_intermediate_2005,
 author       = {Rosalie Iemhoff},
 year         = {2005},
 title        = {Intermediate logics and {Visser}'s rules},
 journal      = {Notre Dame Journal of Formal Logic},
 volume       = {46},
 number       = {1},
 pages        = {65--81},
 doi          = {10.1305/ndjfl/1107220674},
)
@article(kreisel_unableitbarkeitbeweismethode_1957,
 author       = {Georg Kreisel and Hilary Putnam},
 year         = {1957},
 title        = {Eine {Unableitbarkeitsbeweismethode} f\"ur den {Intuitionistischen} {Aussagenkalkül}},
 journal      = {Archiv f\"ur mathematische Logik und Grundlagenforschung},
 volume       = {3},
 number       = {3-4},
 pages        = {74--78},
 doi          = {10.1007/BF01988049},
)
@article(roziere_admissible_1992,
 author       = {Paul Rozi{\`{e}}re},
 year         = {1993},
 title        = {Admissible and Derivable Rules in Intuitionistic Logic},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {3},
 number       = {2},
 pages        = {129--136},
 doi          = {10.1017/S0960129500000165},
)
@book(sorensen_lectures_2006,
 author       = {S{\o}rensen, Morten~Heine and Pawel Urzyczyn},
 year         = {2006},
 title        = {Lectures on the {Curry}-{Howard} isomorphism},
 series       = {Studies in Logic and the Foundations of Mathematics},
 volume       = {149},
 publisher    = {Elsevier},
 doi          = {10.1016/s0049-237x(06)x8001-1},
)
@article(visser_substitutions_2002,
 author       = {Albert Visser},
 year         = {2002},
 title        = {Substitutions of $\Sigma_1^0$-sentences: explorations between intuitionistic propositional logic and intuitionistic arithmetic},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {114},
 number       = {1},
 pages        = {227--271},
 doi          = {10.1016/S0168-0072(01)00081-1},
)