@inproceedings(ager,
 doi          = "10.1145/888251.888254",
)
@article(chapmeister,
 doi          = "10.1017/S0956796809007278",
)
@article(atkey,
 doi          = "10.1017/S095679680900728X",
)
@article(berger,
 doi          = "10.1007/BFb0037100",
)
@article(extraction,
 doi          = "10.1007/s11225-006-6604-5",
)
@inproceedings(biernackis,
)
@article(biernacka,
 doi          = "10.1145/1297658.1297664",
)
@article(stovring,
 doi          = "10.1016/j.entcs.2005.11.056",
)
@article(bove-capretta,
 doi          = "10.1017/S0960129505004822",
)
@incollection(peter-ana:tutorial,
 doi          = "10.1007/978-3-642-03153-3",
)
@phdthesis(edwinI,
)
@inproceedings(edwinII,
 doi          = "10.1007/978-3-540-24849-1\_8",
)
@inproceedings(coquand,
)
@article(cregut,
 doi          = "10.1007/s10990-007-9015-z",
)
@article(curien,
 doi          = "10.1016/0304-3975(91)90230-Y",
)
@inproceedings(danvy-afp,
 doi          = "10.1007/978-3-642-04652-0\_3",
)
@article(danvy:small-step,
 doi          = "10.1016/j.ipl.2007.10.010",
)
@techreport(refocus,
)
@article(cek,
)
@incollection(gandy,
)
@book(hankin,
)
@article(krivine,
 doi          = "10.1007/s10990-007-9018-9",
)
@techreport(zinc,
)
@article(view,
 doi          = "10.1017/S0956796803004829",
)
@phdthesis(norell,
)
@inproceedings(norell:tutorial,
 doi          = "10.1007/978-3-642-04652-0\_5",
)
@inproceedings(oury-swierstra:power-of-pi,
 doi          = "10.1145/1411204.1411213",
)
@book(haskell98,
)
@inproceedings(filip,
)
@article(tait,
 doi          = "10.2307/2271658",
)
@inproceedings(wadler,
 doi          = "10.1145/41625.41653",
)