@inproceedings{9e3ce66e1df54428bfc921ab1560bb95,
title = "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.",
author = "Dawson, {Jeremy E.} and Ranald Clouston and Rajeev Gor{\'e} and Alwen Tiu",
year = "2014",
doi = "10.1007/978-3-662-44602-7_20",
language = "English",
isbn = "9783662446010",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "250--264",
booktitle = "Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Proceedings",
address = "Germany",
note = "8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science, TCS 2014 ; Conference date: 01-09-2014 Through 03-09-2014",
}