Skip to Main content Skip to Navigation
Conference papers

From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic

Abstract : Proof theory for a logic with categorical semantics can be developed by the following methodology: define a sound and complete display calculus for an extension of the logic with additional adjunctions; translate this calculus to a shallow inference nested sequent calculus; translate this calculus to a deep inference nested sequent calculus; then prove this final calculus is sound with respect to the original logic. This complex chain of translations between the different calculi require proofs that are technically intricate and involve a large number of cases, and hence are ideal candidates for formalisation. We present a formalisation of this methodology in the case of Full Intuitionistic Linear Logic (FILL), which is multiplicative intuitionistic linear logic extended with par.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-01402048
Contributor : Hal Ifip <>
Submitted on : Thursday, November 24, 2016 - 10:52:14 AM
Last modification on : Thursday, November 24, 2016 - 11:14:10 AM
Long-term archiving on: : Tuesday, March 21, 2017 - 10:34:08 AM

File

978-3-662-44602-7_20_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Jeremy Dawson, Ranald Clouston, Rajeev Goré, Alwen Tiu. From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. pp.250-264, ⟨10.1007/978-3-662-44602-7_20⟩. ⟨hal-01402048⟩

Share

Metrics

Record views

109

Files downloads

177