@misc(web-appendix,
 author       = {Fabio Alessi et alii},
 year         = {2019},
 title        = {The Web appendix of this paper},
 url          = {https://users.dimi.uniud.it/~alberto.ciaffaglione/LLFP/LFMTP-19.tar.gz},
)
@article(bar02,
 author       = {Henk Barendregt and Erik Barendsen},
 year         = {2002},
 title        = {Autarkic Computations in Formal Proofs},
 journal      = {J. Autom. Reasoning},
 volume       = {28},
 number       = {3},
 pages        = {321--336},
 doi          = {10.1023/A:1015761529444},
)
@inproceedings(CSW14,
 author       = {Chris Casinghino and Vilhelm Sj{\"{o}}berg and Stephanie Weirich},
 year         = {2014},
 title        = {Combining proofs and programs in a dependently typed language},
 editor       = {Jagannathan and Sewell},
 pages        = {33--46},
 doi          = {10.1145/2535838.2535883},
)
@inproceedings(alberto:urm,
 author       = {Alberto Ciaffaglione},
 year         = {2011},
 title        = {A coinductive semantics of the Unlimited Register Machine},
 editor       = {Yu and Wang},
 pages        = {49--63},
 doi          = {10.4204/EPTCS.73.7},
)
@book(Cutland:computability,
 author       = {Nigel Cutland},
 year         = {1980},
 title        = {Computability - An introduction to recursive function theory},
 doi          = {10.1017/CBO9781139171496},
 publisher    = {Cambridge University Press},
)
@inproceedings(FL,
 author       = {Nils Anders Danielsson and John Hughes and Patrik Jansson and Jeremy Gibbons},
 year         = {2006},
 title        = {Fast and loose reasoning is morally correct},
 editor       = {Morrisett and {Peyton Jones}},
 pages        = {206--217},
 doi          = {10.1145/1111037.1111056},
)
@article(HHP-92,
 author       = {Robert Harper and Furio Honsell and Gordon D. Plotkin},
 year         = {1993},
 title        = {A Framework for Defining Logics},
 journal      = {J. {ACM}},
 volume       = {40},
 number       = {1},
 pages        = {143--184},
 doi          = {10.1145/138027.138060},
 note         = {Preliminary version in Proc. of {LICS'87}},
)
@article(HLL06,
 author       = {Furio Honsell and Marina Lenisa and Luigi Liquori},
 year         = {2007},
 title        = {A Framework for Defining Logical Frameworks},
 journal      = {Volume in Honor of G. Plotkin, Electr. Notes Theor. Comput. Sci.},
 volume       = {172},
 pages        = {399--436},
 doi          = {10.1016/j.entcs.2007.02.014},
)
@inproceedings(APLAS,
 author       = {Furio Honsell and Marina Lenisa and Luigi Liquori and Ivan Scagnetto},
 year         = {2016},
 title        = {Implementing Cantor's Paradise},
 editor       = {Igarashi},
 pages        = {229--250},
 doi          = {10.1007/978-3-319-47958-3\_13},
)
@article(honsell:hal-00906391,
 author       = {Furio Honsell and Marina Lenisa and Ivan Scagnetto and Luigi Liquori and Petar Maksimovic},
 year         = {2016},
 title        = {An open logical framework},
 journal      = {J. Log. Comput.},
 volume       = {26},
 number       = {1},
 pages        = {293--335},
 doi          = {10.1093/logcom/ext028},
)
@article(lmcs:3771,
 author       = {Furio Honsell and Luigi Liquori and Petar Maksimovic and Ivan Scagnetto},
 year         = {2017},
 title        = {$\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads},
 journal      = {Logical Methods in Computer Science},
 volume       = {13},
 number       = {3},
 doi          = {10.23638/LMCS-13(3:2)2017},
)
@proceedings(DBLP:conf/aplas/2016,
 editor       = {Atsushi Igarashi},
 year         = {2016},
 title        = {Programming Languages and Systems - 14th Asian Symposium, {APLAS} 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {10017},
 doi          = {10.1007/978-3-319-47958-3},
)
@proceedings(DBLP:conf/popl/2014,
 editor       = {Suresh Jagannathan and Peter Sewell},
 year         = {2014},
 title        = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} '14, San Diego, CA, USA, January 20-21, 2014},
 publisher    = {{ACM}},
 url          = {http://dl.acm.org/citation.cfm?id=2535838},
)
@article(KR1981,
 author       = {H. T. Kung and John T. Robinson},
 year         = {1981},
 title        = {On Optimistic Methods for Concurrency Control},
 journal      = {{ACM} Trans. Database Syst.},
 volume       = {6},
 number       = {2},
 pages        = {213--226},
 doi          = {10.1145/319566.319567},
)
@misc(michielini,
 author       = {Vincent Michielini},
 year         = {2016},
 title        = {\unhbox\voidb@x \hbox{$\mathsf{LLF}_{\mathcal P}$}\ type checker},
 url          = {https://github.com/francescodellamorte/llfp-type-checker},
)
@proceedings(DBLP:conf/popl/2006,
 editor       = {J. Gregory Morrisett and {Peyton Jones}, Simon L.},
 year         = {2006},
 title        = {Proceedings of the 33rd {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2006, Charleston, South Carolina, USA, January 11-13, 2006},
 publisher    = {{ACM}},
 url          = {http://dl.acm.org/citation.cfm?id=1111037},
)
@article(DBLP:journals/iandc/RabeK13,
 author       = {Florian Rabe and Michael Kohlhase},
 year         = {2013},
 title        = {A scalable module system},
 journal      = {Inf. Comput.},
 volume       = {230},
 pages        = {1--54},
 doi          = {10.1016/j.ic.2013.06.001},
)
@proceedings(DBLP:journals/corr/abs-1111-2678,
 editor       = {Fang Yu and Chao Wang},
 year         = {2011},
 title        = {Proceedings 13th International Workshop on Verification of Infinite-State Systems, {INFINITY} 2011, Taipei, Taiwan, 10th October 2011},
 series       = {{EPTCS}},
 volume       = {73},
 doi          = {10.4204/EPTCS.73},
)