The Conditional Logical Framework LFK is a variant of the Harper-Honsell-Plotkin’s 
Edinburgh Logical Framemork LF. It features a generalized form of lambda-abstraction 
where beta-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 beta-reductions corresponding 
to different predicates can be combined in LFK. The framework LFK subsumes, by simple 
instantiation, LF (in fact, it is also a subsystem of LF!), as well as a large class 
of new generalized conditional lambda-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 LFK, such as subject reduction, confluence, strong normalization.