LF+ in Coq for "fast and loose" reasoning
DOI:
https://doi.org/10.6092/issn.1972-5787/9757Keywords:
Type Theory, Logical Frameworks, Computer Aided Formal ReasoningAbstract
We develop the metatheory and the implementation of LF+, and discuss several applications. LF+ capitalizes on research work, carried out by the authors over more than a decade, on Logical Frameworks. It builds on various conservative extensions of LF, which feature "lock"-type constructors, and on the new perspectives offered by its novel "shallow" implementation in Coq. The L^P(N:sigma)[.] constructor, and its binding variant L^P(?x:sigma)[.], 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.Experimenting with "locks" has shown that they are also a very flexible tool for expressing in Type Theory several diverse cognitive attitudes and mental strategies used in ordinary reasoning. These range from the emerging paradigm of "fast and loose reasoning", which trades off efficiency for correctness, as in naive Set Theory, or in computer architecture and distributed systems, when branch prediction and optimistic concurrency control are implemented. Lock-types naturally express also Typical Ambiguity provisos, "squash"' types, and many forms of "reasoning-up-to".
References
F. Alessi, A. Ciaffaglione, P. Di Gianantonio, F. Honsell, and
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.
F. Alessi, A. Ciaffaglione, P. Di Gianantonio, F. Honsell,
M. Lenisa, and I. Scagnetto. The Web appendix of this paper.
https://users.dimi.uniud.it/~alberto.ciaffaglione/LLFP/JFR-19.tar.gz, 2019.
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.
H. Barendregt. Lambda Calculus: its Syntax and Semantics. North Holland, 1984.
H. Barendregt and E. Barendsen. Autarkic computations in
formal proofs. J. Autom. Reasoning, 28(3):321--336, 2002.
doi:10.1023/A:1015761529444.
G. Coulouris, J. Dollimore, and T. Kindberg. Distributed systems - concepts and designs (3. ed.). International computer science series. Addison-Wesley-Longman, 2002.
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.
The Coq Development Team. The Coq Reference Manual - Release 8.8.2. https://coq.inria.fr, 2018.
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.
N. Cutland. Computability - An introduction to recursive function theory. Cambridge University Press, 1980.
J. Chabert, C. Weeks, E. Barbin, J. Borowczyk, J. Chabert,
M. Guillemot, A. Michel-Pajus, A. Djebbar, and J. Martzloff. A
History of Algorithms: From the Pebble to the Microchip. Springer Berlin Heidelberg, 2012. URL https://books.google.it/books?id=XcDqCAAAQBAJ.
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.
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.
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.
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.
F. B. Fitch. Symbolic logic. New York, 1952.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
S. Kripke. Outline of a theory of truth. The journal of philosophy, 72(19):690--716, 1975.
V. Michielini. LLFP type checker. https://github.com/
francescodellamorte/llfp-type-checker, 2016.
P. Martin-Loef and G. Sambin. Intuitionistic type theory, volume 9. Bibliopolis Naples, 1984.
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.
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.
G. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science, 1(2):125--159, 1975.
doi:https://doi.org/10.1016/0304-3975(75)90017-1.
D. Prawitz. Natural Deduction. A Proof Theoretical Study.
Almqvist Wiksell, Stockholm, 1965.
F. Rabe and M. Kohlhase. A scalable module system. Inf. Comput., 230:1--54, 2013. doi:10.1016/j.ic.2013.06.001.
[Uni13] T. Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2019 Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, Ivan Scagnetto
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy
