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.
Type de document :
Communication dans un congrès
Josep Diaz; Ivan Lanese; Davide Sangiorgi. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. Springer, Lecture Notes in Computer Science, LNCS-8705, pp.250-264, 2014, Theoretical Computer Science. 〈10.1007/978-3-662-44602-7_20〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01402048
Contributeur : Hal Ifip <>
Soumis le : jeudi 24 novembre 2016 - 10:52:14
Dernière modification le : jeudi 24 novembre 2016 - 11:14:10
Document(s) archivé(s) le : mardi 21 mars 2017 - 10:34:08

Fichier

978-3-662-44602-7_20_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Jeremy Dawson, Ranald Clouston, Rajeev Goré, Alwen Tiu. From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic. Josep Diaz; Ivan Lanese; Davide Sangiorgi. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. Springer, Lecture Notes in Computer Science, LNCS-8705, pp.250-264, 2014, Theoretical Computer Science. 〈10.1007/978-3-662-44602-7_20〉. 〈hal-01402048〉

Partager

Métriques

Consultations de la notice

44

Téléchargements de fichiers

10