/twelf-proofs

Proofs for type systems and logical systems in Twelf

Twelf Proofs

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.

References

  • Olivier Laurent. Étude de la polarisation en logique. PhD thesis, 2002. PDF.