@misc(coq-manual,
 url          = {https://coq.inria.fr/refman/},
)
@(ml-formalization,
 url          = {https://github.com/harp-project/AML-Formalization/releases/tag/v1.0.6},
)
@inproceedings(appel2007separation,
 doi          = {10.1007/978-3-540-74591-4\_3},
)
@article(nominalcoq,
 doi          = {10.1016/j.entcs.2007.01.028},
)
@inproceedings(poplmark,
 doi          = {10.1007/11541868\_4},
)
@book(CoqArt,
 doi          = {10.1007/978-3-662-07964-5},
)
@inproceedings(k-java,
 doi          = {10.1145/2676726.2676982},
)
@inproceedings(10.1145/3018610.3018616,
 doi          = {10.1145/3018610.3018616},
)
@mastersthesis(carneiro_master,
 url          = {https://github.com/digama0/lean-type-theory/releases/tag/v1.0},
)
@article(ChargueraudLocallyNameless,
 doi          = {10.1007/s10817-011-9225-2},
)
@inproceedings(ChenTrustworthyK,
 doi          = {10.1007/978-3-030-81688-9\_23},
)
@techreport(ChenLucanuRosuInitAlgebraTR,
 url          = {http://hdl.handle.net/2142/107781},
)
@article(ml-explained,
 doi          = {10.1016/j.jlamp.2021.100638},
)
@inproceedings(ChenRosu19Mml,
 doi          = {10.1109/LICS.2019.8785675},
)
@techreport(chen-rosu-2019-tr-mml,
 url          = {http://hdl.handle.net/2142/102281},
)
@article(ChenRosu20Binders,
 doi          = {10.1145/3408970},
)
@article(8133459,
 doi          = {10.1093/logcom/13.6.801},
)
@inproceedings(DPK+19,
 doi          = {10.1145/3314221.3314601},
)
@inproceedings(DMB08,
 doi          = {10.1007/978-3-540-78800-3\_24},
)
@inproceedings(Gordon93,
 doi          = {10.1007/3-540-57826-9\_152},
)
@misc(python-semantics,
 url          = {http://hdl.handle.net/2142/45275},
)
@inproceedings(rv-match,
 doi          = {10.1007/978-3-319-41528-4\_24},
)
@inproceedings(HER15,
 doi          = {10.1145/2813885.2737979},
)
@inproceedings(HSZ+18,
 doi          = {10.1109/CSF.2018.00022},
)
@misc(ml-checker,
 url          = {https://github.com/kframework/matching-logic-proof-checker},
)
@misc(krust-singapore,
 doi          = {10.48550/arXiv.1804.10806},
)
@inproceedings(k-llvm,
 doi          = {10.1145/3445814.3446751},
)
@inproceedings(keller2010importing,
 doi          = {10.1007/978-3-642-14052-5\_22},
)
@article(krebbers2018mosel,
 doi          = {10.1145/3236772},
)
@inproceedings(IrisProofMode,
 doi          = {10.1145/3009837.3009855},
)
@misc(Leroy07alocally,
 url          = {https://xavierleroy.org/POPLmark/locally-nameless/},
)
@misc(stdpp,
 url          = {https://gitlab.mpi-sws.org/iris/stdpp},
)
@inproceedings(McBrideM04,
 doi          = {10.1145/1017472.1017477},
)
@inproceedings(mccreight2009practical,
 doi          = {10.1007/978-3-642-03359-9\_24},
)
@misc(metamath,
 url          = {http://us.metamath.org},
)
@inproceedings(k-js,
 doi          = {10.1145/2737924.2737991},
)
@misc(power1999working,
 url          = {https://mural.maynoothuniversity.ie/6461/1/JP-Working-Linear-Logic.pdf},
)
@article(Rosu17,
 doi          = {10.23638/LMCS-13(4:28)2017},
)
@article(coq-equations,
 doi          = {10.1145/3341690},
)
@article(tarski1955,
 doi          = {10.2140/PJM.1955.5.285},
)
@inproceedings(krust-shanghai,
 doi          = {10.1109/TASE.2018.00014},
)
@misc(wiedijk2007encoding,
 url          = {https://www.cs.ru.nl/~freek/notes/holl2coq.pdf},
)
@article(xavier2018mechanizing,
 doi          = {10.1016/j.entcs.2018.10.014},
)