An open logical framework

DOI10.1093/LOGCOM/EXT028MaRDI QIDQ2804331zbMATH OpenOpenAlexFDO

Authors Furio Honsell, Marina Lenisa, Ivan Scagnetto, Luigi Liquori, Petar Maksimović

Publication date 28 April 2016

Published in Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/10044/1/29759

zbMATH Keywords

computer-aided formal verificationlogical frameworkstype theorytyped lambda calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• A Conditional Logical Framework
• \(\mathsf{LLF}_{\mathcal{P}}\): a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
• Logic representation in LF
• L ax F: Side Conditions and External Evidence as Monads
• A framework for defining logical frameworks

Cited in

(14)

• A semantic framework for proof evidence
• A framework for defining logical frameworks
• Hybridizing a logical framework
• Implementing Cantor's paradise
• scientific article; zbMATH DE number 4180831 (Why is no real title available?)
• A contextual logical framework
• PAL⁺: a lambda-free logical framework
• Plugging-in proof development environments using \textit{locks} in \(\mathsf{LF}\)
• LF+ in Coq for "fast and loose" reasoning
• \(\mathsf{LLF}_{\mathcal{P}}\): a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
• A Conditional Logical Framework
• An open formalism against incompleteness
• 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

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)