References

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

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org