A Definitional Implementation of the Lax Logical Framework LLFP in Coq, for Supporting Fast and Loose Reasoning
| Autor: | Alberto Ciaffaglione, Pietro Di Gianantonio, Fabio Alessi, Marina Lenisa, Furio Honsell |
|---|---|
| Přispěvatelé: | Scagnetto, Ivan |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Correctness [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] Computer science Logical Framework Type Theory Formal Reasoning computer.software_genre lcsh:QA75.5-76.95 Oracle Development (topology) F.4.1 I.2.3 Logical conjunction Formal Reasoning Type Theory Programming language lcsh:Mathematics lcsh:QA1-939 Logic in Computer Science (cs.LO) Logical framework Conceptual framework lcsh:Electronic computers. Computer science Host (network) Optimistic concurrency control computer Logical Framework |
| Zdroj: | LFMTP@LICS Electronic Proceedings in Theoretical Computer Science, Vol 307, Iss Proc. LFMTP 2019, Pp 8-23 (2019) |
| Popis: | The Lax Logical Framework, LLFP, was introduced, by a team including the last two authors, to provide a conceptual framework for integrating different proof development tools, thus allowing for external evidence and for postponing, delegating, or factoring-out side conditions. In particular, LLFP allows for reducing the number of times a proof-irrelevant check is performed. In this paper we give a shallow, actually definitional, implementation of LLFP in Coq, i.e. we use Coq both as host framework and oracle for LLFP. This illuminates the principles underpinning the mechanism of Lock-types and also suggests how to possibly extend Coq with the features of LLFP. The derived proof editor is then put to use for developing case-studies on an emerging paradigm, both at logical and implementation level, which we call fast and loose reasoning following Danielsson et alii [6]. This paradigm trades off efficiency for correctness and amounts to postponing, or running in parallel, tedious or computationally demanding checks, until we are really sure that the intended goal can be achieved. Typical examples are branch-prediction in CPUs and optimistic concurrency control. In Proceedings LFMTP 2019, arXiv:1910.08712 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|