Deep Embedding of Intuitionistic Linear Logic (Q7361302)

In this entry we formalise intuitionistic linear logic (ILL) with a deep embedding of propositions, and shallow and deep embeddings of deductions. We introduce the logic with an explicit exchange rule, meaning sequents have a list of propositions as antecedents. We then prove that sequents that differ only in the order of their antecedents are equivalently valid, representing the alternative implicit exchange rule. The deep embedding of deductions allows for direct construction, manipulation and verification of ILL deductions.