LF+ in Coq for "fast and loose" reasoning

DOI10.6092/issn.1972-5787/9757zbMath1427.68344OpenAlexW2999890999MaRDI QIDQ5210657

Alberto Ciaffaglione, Fabio Alessi, Marina Lenisa, Furio Honsell, Pietro Di Gianantonio, 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)

Uses Software

• Coq
• MMT
• LLFp
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A scalable module system
• Using typed lambda calculus to implement formal systems on a machine
• Notions of computation and monads
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Autarkic computations in formal proofs
• An open logical framework
• A Framework for Defining Logical Frameworks
• L ax F: Side Conditions and External Evidence as Monads
• Implementing Cantor’s Paradise
• A framework for defining logics
• Outline of a Theory of Truth
• Internal type theory
• Plugging-in proof development environments usingLocksinLF
• $\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
• Fast and loose reasoning is morally correct
• Combining proofs and programs in a dependently typed language
• Homotopy Type Theory: Univalent Foundations of Mathematics
• A Conditional Logical Framework

This page was built for publication: LF+ in Coq for "fast and loose" reasoning