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

type theorylogical frameworkstyped lambda calculuscomputer-aided formal verification

Mathematics Subject Classification ID

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

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)

• 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)