A definitional implementation of the Lax logical framework LLF_P in \texttt{Coq}, for supporting fast and loose reasoning

DOI10.4204/EPTCS.307.3MaRDI QIDQ6940468zbMATH OpenFDO

Authors Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa

Publication date 19 August 2025

Copyright license Creative Commons license

Full work available at URL https://doi.org/10.4204/EPTCS.307.3

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• \(\mathsf{LLF}_{\mathcal{P}}\): a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
• 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
• Combining proofs and programs in a dependently typed language
• Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
• Fast and loose reasoning is morally correct
• scientific article; zbMATH DE number 3700811 (Why is no real title available?)
• Implementing Cantor's paradise
• Proceedings 13th International Workshop on Verification of Infinite-State Systems
• Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
• Programming languages and systems. 14th Asian symposium, APLAS 2016, Hanoi, Vietnam, November 21--23, 2016. Proceedings

This page was built for publication: A definitional implementation of the Lax logical framework \(\mathsf{LLF}_{\mathscr{P}}\) in \texttt{Coq}, for supporting fast and loose reasoning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6940468)