LF+ in Coq for "fast and loose" reasoning

DOI10.6092/ISSN.1972-5787/9757MaRDI QIDQ5210657zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

type theorylogical frameworkscomputer-aided formal reasoning

Mathematics Subject Classification ID

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)

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

Cites work

• scientific article; zbMATH DE number 2185657 (Why is no real title available?)
• scientific article; zbMATH DE number 3700811 (Why is no real title available?)
• scientific article; zbMATH DE number 839561 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3076631 (Why is no real title available?)
• A Conditional Logical Framework
• A coinductive semantics of the unlimited register machine
• A framework for defining logical frameworks
• A framework for defining logics
• A scalable module system
• An open logical framework
• Autarkic computations in formal proofs
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Combining proofs and programs in a dependently typed language
• Fast and loose reasoning is morally correct
• Homotopy type theory. Univalent foundations of mathematics
• Implementing Cantor's paradise
• Internal type theory
• L ax F: Side Conditions and External Evidence as Monads
• Notions of computation and monads
• Outline of a Theory of Truth
• Plugging-in proof development environments using \textit{locks} in \(\mathsf{LF}\)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Using typed lambda calculus to implement formal systems on a machine
• \(\mathsf{LLF}_{\mathcal{P}}\): a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads

Cited in

(3)

• Plugging-in proof development environments using \textit{locks} in \(\mathsf{LF}\)
• Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
• \(\mathsf{LLF}_{\mathcal{P}}\): a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads

Describes a project that uses

Uses Software

• GitHub
• LLFp
• MMT
• Coq

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)