Proofs in Twelf.
- Type soundness of simply-typed call-by-value lambda calculus, corresponding to intuitionistic logic.
- Type soundness of LKT, a call-by-name fragment of dual calculi.
- Type soundness of a computational interpretation of LJ (intuitionistic sequent calculus), a call-by-value intuitionistic fragment of LKQ. Moreover, the uniqueness of the operational semantics is proved.
- Admissibility of cuts in Kleene's G3-style sequent calculus for intuitionistic propositional logic.
- "Positive formula" lemma for MALLP [Laurent 2002], a multiplicative/additive fragment of polarized linear logic.
- Olivier Laurent. Étude de la polarisation en logique. PhD thesis, 2002. PDF.