Recommendations
Cited in
(14)- Plugging-in proof development environments using \textit{locks} in \(\mathsf{LF}\)
- scientific article; zbMATH DE number 4180831 (Why is no real title available?)
- A framework for defining logical frameworks
- A contextual logical framework
- Implementing Cantor's paradise
- PAL+: a lambda-free logical framework
- Hybridizing a logical framework
- LF+ in Coq for "fast and loose" reasoning
- A Conditional Logical Framework
- An open formalism against incompleteness
- A semantic framework for proof evidence
- Gluing together proof environments: canonical extensions of LF type theories featuring locks
- A definitional implementation of the Lax logical framework \(\mathsf{LLF}_{\mathscr{P}}\) in \texttt{Coq}, for supporting fast and loose reasoning
- \(\mathsf{LLF}_{\mathcal{P}}\): a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
This page was built for publication: An open logical framework
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2804331)