LF+ in Coq for "fast and loose" reasoning
DOI10.6092/ISSN.1972-5787/9757zbMATH Open1427.68344OpenAlexW2999890999MaRDI QIDQ5210657FDOQ5210657
Authors: Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, Ivan Scagnetto 
Publication date: 21 January 2020
Full work available at URL: https://doi.org/10.6092/issn.1972-5787/9757
Recommendations
- Coalgebraic Reasoning in Coq: Bisimulation and the λ-Coiteration Scheme
- \textsf{LOGIC}: a Coq library for logics
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Towards a practical library for monadic equational reasoning in Coq
- Mechanizing focused linear logic in Coq
- An implementation of LF with coercive subtyping and universes
- Formalization of a λ-calculus with explicit substitutions in Coq
- Formalizing cut elimination of coalgebraic logics in Coq
- scientific article; zbMATH DE number 1927413
Logic in computer science (03B70) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38)
Cites Work
- \(\mathsf{LLF}_{\mathcal{P}}\): a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
- Outline of a Theory of Truth
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- A scalable module system
- A framework for defining logics
- Title not available (Why is that?)
- Notions of computation and monads
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Homotopy type theory. Univalent foundations of mathematics
- Title not available (Why is that?)
- Internal type theory
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Autarkic computations in formal proofs
- Using typed lambda calculus to implement formal systems on a machine
- A Conditional Logical Framework
- A framework for defining logical frameworks
- An open logical framework
- Combining proofs and programs in a dependently typed language
- Fast and loose reasoning is morally correct
- A coinductive semantics of the unlimited register machine
- L ax F: Side Conditions and External Evidence as Monads
- Implementing Cantor's paradise
- Plugging-in proof development environments using \textit{locks} in \(\mathsf{LF}\)
Cited In (3)
Uses Software
This page was built for publication: LF+ in Coq for "fast and loose" reasoning
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5210657)
