Linear logic as a logical framework

International audienceLogical frameworks have seen three decades of design, theory, implementation , and applications. An early example of such a framework was LF (Honsell, Harper, & Plotkin, LICS 1987): that dependently typed λ-calculus provided a framework for defining the syntax of terms and formulas as well as natural deduction proofs in various intuitionistic logics. In a series of papers starting in 1994, several researchers (see references below) have also made use of linear logic (with or without subexponentials) as a framework for specifying a range of proof systems. Simple theories in linear logic are able to specify various proof systems for first-order logics that include sequent calculus (both single-conclusion and multiple-conclusion), natural deduction (possibly with generalized elimination rules), free deduction, and tableaux. There is also a simple decision procedure that can guarantee the ad-missibility of cuts and (non-atomic) initials rules by analyzing the linear logic specification of rules. Finally, since proof search in linear logic can be implemented , computer systems exist that can emulate these various proof systems given their linear logic specification. In this talk, I plan to overview this work and attempt to find a more lightweight formulation of this logical framework that does not need to explicitly reference a metalogic involving linear logic and subexponentials