A Conditional Logical Framework

Abstract The Conditional Logical Framework LF K is a variant of the Harper-Honsell-Plotkin’s Edinburgh Logical Framemork LF. It features a generalized form of λ -abstraction where β -reductions fire under the condition that the argument satisfies a logical predicate. The key idea is that the type system memorizes under what conditions and where reductions have yet to fire. Different notions of β -reductions corresponding to different predicates can be combined in LF K. The framework LF K subsumes, by simple instantiation, LF (in fact, it is also a subsystem of LF!), as well as a large class of new generalized conditional λ -calculi. These are appropriate to deal smoothly with the side-conditions of both Hilbert and Natural Deduction presentations of Modal Logics. We investigate and characterize the metatheoretical properties of the calculus underpinning LF K, such as subject reduction, confluence, strong normalization.

Authors

• Furio Honsell
• Marina Lenisa
• Luigi Liquori
• Ivan Scagnetto

Keywords

No keywords are indexed for this paper.