%0 Conference Proceedings
%T From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic
%+ Australian National University (ANU)
%+ Aarhus University [Aarhus]
%+ Nanyang Technological University [Singapour]
%A Dawson, Jeremy, E.
%A Clouston, Ranald
%A Goré, Rajeev
%A Tiu, Alwen
%Z Part 2: Track B: Logic, Semantics, Specification and Verification
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 8th IFIP International Conference on Theoretical Computer Science (TCS)
%C Rome, Italy
%Y Josep Diaz
%Y Ivan Lanese
%Y Davide Sangiorgi
%I Springer
%3 Theoretical Computer Science
%V LNCS-8705
%P 250-264
%8 2014-09-01
%D 2014
%R 10.1007/978-3-662-44602-7_20
%Z Computer Science [cs]Conference papers
%X 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.
%G English
%Z TC 1
%Z TC 2
%Z WG 2.2
%2 https://inria.hal.science/hal-01402048/document
%2 https://inria.hal.science/hal-01402048/file/978-3-662-44602-7_20_Chapter.pdf
%L hal-01402048
%U https://inria.hal.science/hal-01402048
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC2
%~ IFIP-LNCS-8705
%~ IFIP-TCS
%~ IFIP-WG2-2