An open logical framework

DOI10.1093/LOGCOM/EXT028zbMATH Open1352.68061OpenAlexW1999838273MaRDI QIDQ2804331FDOQ2804331

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

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

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)

Cited In (12)

• Plugging-in proof development environments using \textit{locks} in \(\mathsf{LF}\)
• Title not available (Why is that?)
• 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
• \(\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)