F. Alessi, The Web appendix of this paper, 2019.

H. Barendregt and &. Barendsen, Autarkic Computations in Formal Proofs, J. Autom. Reasoning, vol.28, issue.3, pp.321-336, 2002.

C. Casinghino, V. Sjöberg-&-stephanie, and . Weirich, Combining proofs and programs in a dependently typed language, Jagannathan & Sewell [13, pp.33-46, 2014.
DOI : 10.1145/2535838.2535883
URL : https://repository.upenn.edu/cgi/viewcontent.cgi?article=2031&context=cis_reports

A. Ciaffaglione, A coinductive semantics of the Unlimited Register Machine, vol.18, pp.49-63, 2011.

N. Cutland, Computability -An introduction to recursive function theory, 1980.

, Fast and loose reasoning is morally correct, vol.16, pp.206-217, 2006.

R. Harper, F. Honsell-&-gordon, and D. Plotkin, A Framework for Defining Logics, Preliminary version in Proc. of LICS'87, vol.40, pp.143-184, 1993.

F. Honsell, M. Lenisa-&-luigi, and . Liquori, A Framework for Defining Logical Frameworks, Plotkin, Electr. Notes Theor. Comput. Sci, vol.172, pp.399-436, 2007.
URL : https://hal.archives-ouvertes.fr/hal-01148312

F. Honsell, M. Lenisa, L. Liquori-&-ivan, and . Scagnetto, Implementing Cantor's Paradise, pp.229-250, 2016.

F. Honsell, M. Lenisa, I. Scagnetto, L. Liquori-&-petar, and . Maksimovic, An open logical framework, J. Log. Comput, vol.26, issue.1, pp.293-335, 2016.
URL : https://hal.archives-ouvertes.fr/hal-00906391

F. Honsell, L. Liquori, P. Maksimovic-&-ivan, and . Scagnetto, LLF P : a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads, Logical Methods in Computer Science, vol.13, issue.3, 2017.

, Programming Languages and Systems -14th Asian Symposium, vol.10017, 2016.

, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, 2014.

H. T. Kung-&-john and T. Robinson, On Optimistic Methods for Concurrency Control, ACM Trans. Database Syst, vol.6, issue.2, pp.213-226, 1981.

V. Michielini, LLF P type checker, 2016.

, Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006.

F. Rabe and &. Michael-kohlhase, A scalable module system, Inf. Comput, vol.230, pp.1-54, 2013.

, Proceedings 13th International Workshop on Verification of InfiniteState Systems, vol.73, 2011.