An open logical framework

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

Luigi Liquori, Furio Honsell, Marina Lenisa, Ivan Scagnetto, 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 (8)

• Title not available (Why is that?)
• PAL⁺: a lambda-free logical framework
• LF+ in Coq for "fast and loose" reasoning
• Plugging-in proof development environments usingLocksinLF
• Implementing Cantor’s Paradise
• A Conditional Logical Framework
• An open formalism against incompleteness
• A semantic framework for proof evidence

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)