×

\(\mathrm{LF}^+\) in Coq for fast-and-loose reasoning. (English) Zbl 1427.68344

Summary: We develop the metatheory and the implementation, in Coq, of \(\mathrm{LF}^+\), and discuss several applications. \(\mathrm{LF}^+\) generalises research work, carried out by the authors over more than a decade, on Logical Frameworks conservatively extending LF and featuring lock-type constructors \(\mathcal L^{\mathcal P(N:\sigma)}\llbracket\cdot\rrbracket\). Lock-types capture monadically the concept of inhabitability up-to. They were originally introduced for factoring-out, postponing, or delegating to external tools the verification of time-consuming judgments, which are morally proof-irrelevant, thus allowing for integrating different sources of epistemic evidence in a unique Logical Framework. Besides introducing \(\mathrm{LF}^+\) and its “shallow” implementation in Coq, the main novelty of the paper is to show that lock-types are also a very flexible tool for expressing in Type Theory several diverse cognitive attitudes and mental strategies used in ordinary reasoning, which essentially amount to reasoning up-to, as in e.g. Typical Ambiguity provisos or co-inductive Coq proofs. In particular we address the encoding of the emerging paradigm of fast-and-loose reasoning, which trades off efficiency for correctness. This paradigm, implicitly used normally in naïve Set Theory, is producing considerable impact also in computer architecture and distributed systems, when branch prediction and optimistic concurrency control are implemented

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B38 Type theory
03B70 Logic in computer science
68V20 Formalization of mathematics in connection with theorem provers

Software:

GitHub; MMT; LLFp; Coq
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] F. Alessi, A. Ciaffaglione, P. Di Gianantonio, F. Honsell, and
[2] M. Lenisa. A definitional implementation of the Lax Logical Framework LLFP in Coq, for supporting fast and loose reasoning. In LFMTP 2019 Logical Frameworks and Meta-Languages: Theoryand Practice 2019, Vancouver, Canada, June 2019. URL https://hal.archives-ouvertes.fr/hal-02152406.
[3] F. Alessi, A. Ciaffaglione, P. Di Gianantonio, F. Honsell,
[4] M. Lenisa, and I. Scagnetto. The Web appendix of this paper.
[5] https://users.dimi.uniud.it/ alberto.ciaffaglione/LLFP/JFR-19.tar.gz, 2019.
[6] A. Avron, F. Honsell, I.Mason, and R. Pollack. Using Typed Lambda Calculus to Implement Formal Systems on a Machine. Journal of Automated Reasoning, 9(3):309-354, 1992. · Zbl 0784.68072
[7] H. Barendregt. Lambda Calculus: its Syntax and Semantics. North Holland, 1984. · Zbl 0551.03007
[8] H. Barendregt and E. Barendsen. Autarkic computations in · Zbl 1002.68156
[9] formal proofs. J. Autom. Reasoning, 28(3):321-336, 2002. · Zbl 1002.68156
[10] doi:10.1023/A:1015761529444.
[11] G. Coulouris, J. Dollimore, and T. Kindberg. Distributed systems - concepts and designs (3. ed.). International computer science series. Addison-Wesley-Longman, 2002. · Zbl 0848.68021
[12] A. Ciaffaglione. A coinductive semantics of the unlimited register machine. In F. Yu and C. Wang, editors, Proceedings 13th International Workshop on Verification of Infinite-State Systems, INFINITY 2011, Taipei, Taiwan, 10th October 2011., volume 73 of EPTCS, pages 49-63, 2011. doi:10.4204/EPTCS.73.7. · Zbl 1457.68161
[13] The Coq Development Team. The Coq Reference Manual - Release 8.8.2. https://coq.inria.fr, 2018.
[14] C. Casinghino, V. Sjoeberg, and S. Weirich. Combining proofs and programs in a dependently typed language. In S. Jagannathan and P. Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, pages 33-46. ACM, 2014. doi:10.1145/2535838.2535883. · Zbl 1284.68125
[15] N. Cutland. Computability - An introduction to recursive function theory. Cambridge University Press, 1980. · Zbl 0448.03029
[16] J. Chabert, C. Weeks, E. Barbin, J. Borowczyk, J. Chabert,
[17] M. Guillemot, A. Michel-Pajus, A. Djebbar, and J. Martzloff. A
[18] History of Algorithms: From the Pebble to the Microchip. Springer Berlin Heidelberg, 2012. URL https://books.google.it/books?id=XcDqCAAAQBAJ.
[19] J. Despeyroux, A. Felty, and A. Hirschowitz. Higher-order abstract syntax in coq. In M. Dezani-Ciancaglini and G. Plotkin, editors, Typed Lambda Calculi and Applications, pages 124-138, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. · Zbl 1063.68650
[20] J. Despeyroux and A. Hirschowitz. Higher-order abstract syntax with induction in coq. In F. Pfenning, editor, Logic Programming and Automated Reasoning, pages 159-173, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg.
[21] N. A. Danielsson, J. Hughes, P. Jansson, and J. Gibbons. Fast and loose reasoning is morally correct. In J. G. Morrisett and S. L. Peyton Jones, editors, Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, pages 206-217. ACM, 2006. doi:10.1145/1111037.1111056. · Zbl 1370.68042
[22] P. Dybjer. Internal type theory. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs, pages 120-134, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. · Zbl 1434.03149
[23] F. B. Fitch. Symbolic logic. New York, 1952. · Zbl 0049.00504
[24] R. Harper, F. Honsell, and G. D. Plotkin. A framework for defining logics. J. ACM, 40(1):143-184, 1993. doi:10.1145/138027.138060. Preliminary version in Proc. of LICS’87. · Zbl 0778.03004
[25] F. Honsell, M. Lenisa, and L. Liquori. A framework for defining logical frameworks. Volume in Honor of G. Plotkin, Electr. Notes Theor. Comput. Sci., 172:399-436, 2007. doi:10.1016/j.entcs.2007.02.014. · Zbl 1277.03029
[26] F. Honsell, M. Lenisa, L. Liquori, P. Maksimovic, and I. Scagnetto. Lfp: A logical framework with external predicates. In Proceedings of the Seventh International Workshop on Logical Frameworks and Meta-languages, Theory and Practice, LFMTP ’12, pages 13-22, New York, NY, USA, 2012. ACM. doi:10.1145/2364406.2364409. · Zbl 1352.68061
[27] F. Honsell, M. Lenisa, L. Liquori, and I. Scagnetto. A conditional logical framework. In LPAR’08, volume 5330 of LNCS, pages 143-157. Springer-Verlag, 2008. · Zbl 1182.03068
[28] F. Honsell, M. Lenisa, L. Liquori, and I. Scagnetto. Implementing cantor’s paradise. In A. Igarashi, editor, Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, volume 10017 of Lecture Notes in Computer Science, pages 229-250, 2016. doi:10.1007/978-3-319-47958-3 13. · Zbl 1485.03031
[29] F. Honsell, L. Liquori, P. Maksimovic, and I. Scagnetto. Gluing together proof environments: Canonical extensions of LF type theories featuring locks. In I. Cervesato and K. Chaudhuri, editors, Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, LFMTP 2015, Berlin, Germany, 1 August 2015., volume 185 of EPTCS, pages 3-17, 2015. doi:10.4204/EPTCS.185.1.
[30] F. Honsell, L. Liquori, P. Maksimovic, and I. Scagnetto. LLFP: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads. Logical Methods in Computer Science, 13(3), 2017. doi:10.23638/LMCS-13(3:2)2017. · Zbl 1456.03027
[31] F. Honsell, L. Liquori, P. Maksimovic, and I. Scagnetto. Plugging in proof development environments using Locks in LF. Mathematical Structures in Computer Science, 28(9):15781605, 2018. doi:10.1017/S0960129518000105. · Zbl 1400.68195
[32] F. Honsell, L. Liquori, and I. Scagnetto. LaxF: Side Conditions and External Evidence as Monads. In Proc. of MFCS 2014 (39th International Symposium on Mathematical Foundations of Computer Science), Part I, volume 8634 of Lecture Notes in Computer Science, pages 327-339, Budapest, Hungary, August 2014. Springer. · Zbl 1425.68071
[33] F. Honsell, M. Lenisa, I. Scagnetto, L. Liquori, and P. Maksimovic. An open logical framework. J. Log. Comput., 26(1):293-335, 2016. doi:10.1093/logcom/ext028. · Zbl 1352.68061
[34] F. Honsell. 25 years of formal proof cultures: Some problems, some philosophy, bright future. In Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP’13, pages 37-42, New York, NY, USA, 2013. ACM. doi:10.1145/2503887.2503896.
[35] D. A. Jimenez, S. W. Keckler, and C. Lin. The impact of delay on the design of branch predictors. In A. Wolfe and M. S. Schlansker, editors, Proceedings of the 33rd Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 33, Monterey, California, USA, December 10-13, 2000, pages 67-76. ACM/IEEE Computer Society, 2000. doi:10.1109/MICRO.2000.898059.
[36] H. T. Kung and J. T. Robinson. On optimistic methods for concurrency control. ACM Trans. Database Syst., 6(2):213-226, 1981. doi:10.1145/319566.319567.
[37] S. Kripke. Outline of a theory of truth. The journal of philosophy, 72(19):690-716, 1975. · Zbl 0952.03513
[38] V. Michielini. LLFP type checker. https://github.com/
[39] francescodellamorte/llfp-type-checker, 2016.
[40] P. Martin-Loef and G. Sambin. Intuitionistic type theory, volume 9. Bibliopolis Naples, 1984.
[41] E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55-92, 1991. doi:https://doi.org/10.1016/0890-5401(91)90052-4. Selections from 1989 IEEE Symposium on Logic in Computer Science. · Zbl 0723.68073
[42] D. Mueller and F. Rabe. Rapid Prototyping Formal Systems in MMT: 5 Case Studies. In LFMTP 2019 Logical Frameworks and Meta-Languages: Theory and Practice 2019, Vancouver, Canada, June 2019. URL https://hal.archives-ouvertes.fr/hal-02150167.
[43] G. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science, 1(2):125-159, 1975. · Zbl 0325.68006
[44] doi:https://doi.org/10.1016/0304-3975(75)90017-1.
[45] D. Prawitz. Natural Deduction. A Proof Theoretical Study. · Zbl 0173.00205
[46] Almqvist Wiksell, Stockholm, 1965. · Zbl 0173.00205
[47] F. Rabe and M. Kohlhase. A scalable module system. Inf. Comput., 230:1-54, 2013. doi:10.1016/j.ic.2013.06.001. · Zbl 1358.68283
[48] [Uni13] T. Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013. · Zbl 1298.03002
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.