@article{AcclHornStra:22:An-Analy:wo,
	author = {Acclavio, Matteo and Horne, Ross and Straßburger, Lutz},
	date-added = {2022-11-02 19:39:44 +0000},
	date-modified = {2022-11-02 19:39:44 +0000},
	doi = {10.46298/lmcs-18(4:1)2022},
	journal = {Logical Methods in Computer Science},
	keywords = {deep inference},
	number = {4},
	pages = {1:1--80},
	title = {An Analytic Propositional Proof System on Graphs},
	url = {https://arxiv.org/abs/2012.01102},
	volume = {18},
	year = {2022},
	bdsk-url-1 = {https://doi.org/10.46298/lmcs-18(4:1)2022}}

@inproceedings{AcclHornMauwStra:22:A-Graphi:cz,
	author = {Acclavio, Matteo and Horne, Ross and Mauw, Sjouke and Straßburger, Lutz},
	booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD)},
	date-added = {2022-11-02 19:39:44 +0000},
	date-modified = {2022-11-02 19:39:44 +0000},
	doi = {10.4230/LIPICS.FSCD.2022.22},
	editor = {Felty, Amy P.},
	keywords = {deep inference},
	pages = {22:1--25},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {A Graphical Proof Theory of Logical Time},
	url = {https://drops.dagstuhl.de/opus/volltexte/2022/16303/pdf/LIPIcs-FSCD-2022-22.pdf},
	volume = {228},
	year = {2022},
	bdsk-url-1 = {https://drops.dagstuhl.de/opus/volltexte/2022/16303/},
	bdsk-url-2 = {https://doi.org/10.4230/LIPICS.FSCD.2022.22}}

@inproceedings{AcclGuer:20:A-Deep-I:gw,
	author = {Acclavio, Matteo and Guerrieri, Giulio},
	booktitle = {Linearity \& Trends in Linear Logic and Applications (Linearity\&TLLA)},
	date-added = {2022-11-02 19:39:44 +0000},
	date-modified = {2022-11-02 19:39:44 +0000},
	doi = {10.4204/eptcs.353.2},
	editor = {Dal Lago, Ugo and de Paiva, Valeria},
	keywords = {deep inference},
	pages = {26--49},
	publisher = {Open Publishing Association},
	series = {Electronic Proceedings in Theoretical Computer Science},
	title = {A Deep Inference System for Differential Linear Logic},
	url = {https://arxiv.org/pdf/2112.14963.pdf},
	volume = {353},
	year = {2020},
	bdsk-url-1 = {https://doi.org/10.4204%2Feptcs.353.2},
	bdsk-url-2 = {https://doi.org/10.4204/eptcs.353.2}}

@inproceedings{Accl:20:Exponent:lk,
	author = {Acclavio, Matteo},
	booktitle = {Linearity \& Trends in Linear Logic and Applications (Linearity\&TLLA)},
	date-added = {2022-11-02 19:39:44 +0000},
	date-modified = {2022-11-02 19:39:44 +0000},
	doi = {10.4204/eptcs.353.1},
	editor = {Dal Lago, Ugo and de Paiva, Valeria},
	keywords = {deep inference},
	pages = {1--25},
	publisher = {Open Publishing Association},
	series = {Electronic Proceedings in Theoretical Computer Science},
	title = {Exponentially Handsome Proof Nets and Their Normalization},
	url = {https://arxiv.org/pdf/2112.14962.pdf},
	volume = {353},
	year = {2020},
	bdsk-url-1 = {https://doi.org/10.4204/eptcs.353.1}}

@inproceedings{AcclHornStra:20:Logic-Be:gy,
	author = {Acclavio, Matteo and Horne, Ross and Straßburger, Lutz},
	booktitle = {35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
	date-added = {2020-12-09 19:57:18 +0000},
	date-modified = {2020-12-09 20:13:01 +0000},
	doi = {10.1145/3373718.3394763},
	editor = {Kobayashi, Naoki},
	keywords = {deep inference},
	pages = {38--52},
	publisher = {ACM},
	title = {Logic Beyond Formulas: {A} Proof System on Graphs},
	url = {https://satoss.uni.lu/members/ross/pdf/LBF.pdf},
	year = {2020},
	bdsk-url-1 = {https://satoss.uni.lu/members/ross/pdf/LBF.pdf},
	bdsk-url-2 = {https://doi.org/10.1145/3373718.3394763}}

@article{AlenOlivPozz:13:Nested-S:xw,
	author = {Alenda, Régis and Olivetti, Nicola and Pozzato, Gian Luca},
	date-added = {2014-04-26 16:03:05 +0000},
	date-modified = {2016-04-13 11:26:39 +0000},
	doi = {10.1093/logcom/ext034},
	journal = {Journal of Logic and Computation},
	keywords = {deep inference},
	number = {1},
	pages = {7--50},
	title = {Nested Sequent Calculi for Normal Conditional Logics},
	url = {http://www.di.unito.it/~pozzato/papers/JLC2013.pdf},
	volume = {26},
	year = {2016},
	bdsk-url-1 = {http://www.di.unito.it/~pozzato/papers/JLC2013.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1093/logcom/ext034}}

@inproceedings{alenda2012nested,
	author = {Alenda, Régis and Olivetti, Nicola and Pozzato, Gian Luca},
	booktitle = {Logics in Artificial Intelligence (JELIA)},
	date-added = {2013-03-05 20:13:34 +0000},
	date-modified = {2016-12-31 10:11:37 +0000},
	doi = {10.1007/978-3-642-33353-8\_2},
	editor = {Fariñas del Cerro, Luis and Herzig, Andreas and Mengin, Jérôme},
	keywords = {deep inference},
	pages = {14--27},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Nested Sequent Calculi for Conditional Logics},
	url = {http://www.di.unito.it/~argo/papers/2012_JELIAb.pdf},
	volume = {7519},
	year = {2012},
	bdsk-url-1 = {http://www.di.unito.it/~argo/papers/2012_JELIAb.pdf}}

@article{AlerGugl:18:Subatomi:ty,
	author = {Aler Tubella, Andrea and Guglielmi, Alessio},
	date-added = {2017-03-31 14:28:52 +0000},
	date-modified = {2023-05-26 17:40:29 +0100},
	doi = {10.1145/3173544},
	journal = {ACM Transactions on Computational Logic},
	keywords = {deep inference},
	number = {1},
	pages = {5:1--33},
	title = {Subatomic Proof Systems: {S}plittable Systems},
	url = {https://arxiv.org/pdf/1703.10258.pdf},
	volume = {19},
	year = {2018},
	bdsk-url-1 = {https://arxiv.org/pdf/1703.10258.pdf}}

@inproceedings{AlerGuglRalp:17:Removing:oq,
	author = {Aler Tubella, Andrea and Guglielmi, Alessio and Ralph, Benjamin},
	booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL)},
	date-added = {2017-06-20 09:56:44 +0000},
	date-modified = {2017-08-18 14:23:13 +0000},
	doi = {10.4230/LIPIcs.CSL.2017.9},
	editor = {Goranko, Valentin and Dam, Mads},
	keywords = {deep inference},
	pages = {9:1--17},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {Removing Cycles from Proofs},
	url = {http://drops.dagstuhl.de/opus/volltexte/2017/7700/pdf/LIPIcs-CSL-2017-9.pdf},
	volume = {82},
	year = {2017},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/RCP.pdf}}

@phdthesis{Aler:16:A-Study-:hc,
	author = {Aler Tubella, Andrea},
	date-added = {2017-02-09 07:14:34 +0000},
	date-modified = {2018-03-23 19:39:13 +0000},
	keywords = {deep inference},
	school = {University of Bath},
	title = {A Study of Normalisation Through Subatomic Logic},
	url = {https://people.bath.ac.uk/ag248/aat/phd.pdf},
	year = {2017},
	bdsk-url-1 = {https://aalertubelladotcom.files.wordpress.com/2017/02/thesis.pdf}}

@article{ArisDasStra:15:On-Neste:df,
	author = {Arisaka, Ryuta and Das, Anupam and Straßburger, Lutz},
	date-added = {2016-04-13 10:55:57 +0000},
	date-modified = {2016-04-13 10:59:46 +0000},
	doi = {10.2168/LMCS-11(3:7)2015},
	journal = {Logical Methods in Computer Science},
	keywords = {deep inference},
	number = {3},
	pages = {7:1--33},
	title = {On Nested Sequents for Constructive Modal Logics},
	url = {http://arxiv.org/pdf/1505.06896.pdf},
	volume = {11},
	year = {2015},
	bdsk-url-1 = {http://arxiv.org/pdf/1505.06896.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.2168/LMCS-11(3:7)2015}}

@article{BarrGugl:22:A-Subato:yr,
	author = {Barrett, Chris and Guglielmi, Alessio},
	date-added = {2022-11-02 19:39:44 +0000},
	date-modified = {2022-11-02 19:39:44 +0000},
	doi = {10.1145/3545116},
	journal = {ACM Transactions on Computational Logic},
	keywords = {deep inference},
	number = {4},
	pages = {26:1--25},
	title = {A Subatomic Proof System for Decision Trees},
	url = {https://arxiv.org/pdf/2105.01382.pdf},
	volume = {23},
	year = {2022},
	bdsk-url-1 = {https://doi.org/10.1145/3545116}}

@inproceedings{BarrGugl:21:Totally-:zm,
	author = {Barrett, Victoria and Guglielmi, Alessio},
	booktitle = {5th International Workshop on Trends in Linear Logic and Applications (TLLA)},
	date-added = {2021-06-28 12:20:08 +0100},
	date-modified = {2022-11-02 19:55:31 +0000},
	keywords = {deep inference},
	pages = {1--7},
	title = {Totally Linear Proofs},
	url = {https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271417},
	year = {2021},
	bdsk-url-1 = {https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271417}}

@inproceedings{Bilk:11:A-Note-o:fk,
	author = {Bílková, Marta},
	booktitle = {Logic, Language, and Computation (TbiLLC 2009)},
	date-added = {2013-03-05 19:49:05 +0000},
	date-modified = {2016-12-31 18:48:28 +0000},
	doi = {10.1007/978-3-642-22303-7\_3},
	editor = {Bezhanishvili, Nick and Löbner, Sebastian and Schwabe, Kerstin and Spada, Luca},
	keywords = {deep inference},
	pages = {30--45},
	publisher = {Springer},
	series = {Lecture Notes in Artificial Intelligence},
	title = {A Note on Uniform Interpolation Proofs in Modal Deep Inference Calculi},
	volume = {6618},
	year = {2011},
	bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-22303-7%5C_3}}

@article{BlutPanaSlav:09:Deep-Inf:kb,
	author = {Blute, Richard and Panangaden, Prakash and Slavnov, Sergey},
	date-added = {2009-03-19 15:12:35 +0100},
	date-modified = {2014-04-11 00:43:36 +0000},
	doi = {10.1007/s10485-010-9241-0},
	journal = {Applied Categorical Structures},
	keywords = {deep inference},
	pages = {209--228},
	title = {Deep Inference and Probabilistic Coherence Spaces},
	url = {http://www.cs.mcgill.ca/~prakash/Pubs/seqcats.pdf},
	volume = {20},
	year = {2012},
	bdsk-url-1 = {http://www.cs.mcgill.ca/~prakash/Pubs/seqcats.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/s10485-010-9241-0}}

@incollection{BlutGuglIvanPana:10:A-Logica:uq,
	author = {Blute, Richard F. and Guglielmi, Alessio and Ivanov, Ivan T. and Panangaden, Prakash and Straßburger, Lutz},
	booktitle = {Categories and Types in Logic, Language, and Physics},
	date-added = {2010-06-01 10:20:30 +0200},
	date-modified = {2014-04-10 22:23:03 +0000},
	doi = {10.1007/978-3-642-54789-8\_6},
	editor = {Casadio, Claudia and Coecke, Bob and Moortgat, Michael and Scott, Philip},
	keywords = {deep inference},
	pages = {90--107},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {A Logical Basis for Quantum Evolution and Entanglement},
	url = {https://people.bath.ac.uk/ag248/p/LBQEE.pdf},
	volume = {8222},
	year = {2014},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/LBQEE.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-54789-8%5C_6}}

@misc{BlutPanaStra:08:The-Logi:lh,
	author = {Blute, Rick and Panangaden, Prakash and Straßburger, Lutz},
	booktitle = {Trends in Logic {VI}: {L}ogic and the Foundations of Physics: {S}pace, Time and Quanta},
	date-added = {2009-03-19 14:38:26 +0100},
	date-modified = {2015-02-08 11:48:46 +0000},
	keywords = {deep inference},
	title = {The Logic {BV} and Quantum Causality},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/BVlocative.pdf},
	year = {2008},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/BVlocative.pdf}}

@inproceedings{BrusStra:17:On-the-L:qr,
	author = {Bruscoli, Paola and Straßburger, Lutz},
	booktitle = {24th International Workshop on Logic, Language, Information, and Computation (WoLLIC)},
	date-added = {2017-07-14 08:51:55 +0000},
	date-modified = {2017-09-01 10:16:16 +0000},
	doi = {10.1007/978-3-662-55386-2\_5},
	editor = {Kennedy, Juliette and de Queiroz, Ruy J.G.B.},
	keywords = {deep inference},
	pages = {68--79},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {On the Length of Medial-Switch-Mix Derivations},
	url = {http://opus.bath.ac.uk/56221/1/sm_length.pdf},
	volume = {10388},
	year = {2017},
	bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-662-55386-2%5C_5}}

@article{BrusGuglGundPari:09:Quasipol:kx,
	author = {Bruscoli, Paola and Guglielmi, Alessio and Gundersen, Tom and Parigot, Michel},
	date-added = {2009-03-25 12:29:53 +0100},
	date-modified = {2017-12-04 12:09:05 +0000},
	doi = {10.2168/LMCS-12(2:5)2016},
	journal = {Logical Methods in Computer Science},
	keywords = {deep inference},
	number = {1},
	pages = {5:1--30},
	title = {Quasipolynomial Normalisation in Deep Inference Via Atomic Flows and Threshold Formulae},
	url = {https://lmcs.episciences.org/1637/pdf},
	volume = {12},
	year = {2016},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/QuasiPolNormDI.pdf}}

@misc{BrusGuglGundPari:11:A-Quasip:uq,
	author = {Bruscoli, Paola and Guglielmi, Alessio and Gundersen, Tom and Parigot, Michel},
	date-added = {2010-01-25 08:58:41 +0100},
	date-modified = {2015-10-07 23:39:44 +0000},
	keywords = {deep inference},
	title = {A Quasipolynomial Normalisation Procedure in Deep Inference},
	url = {https://people.bath.ac.uk/ag248/p/QPNPDI.pdf},
	year = {2011},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/QPNPDI.pdf}}

@inproceedings{BrusGuglGundPari:09:A-Quasip:fk,
	author = {Bruscoli, Paola and Guglielmi, Alessio and Gundersen, Tom and Parigot, Michel},
	booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-16)},
	date-added = {2011-05-04 17:41:54 +0100},
	date-modified = {2015-04-13 09:46:45 +0000},
	doi = {10.1007/978-3-642-17511-4\_9},
	editor = {Clarke, Edmund M. and Voronkov, Andrei},
	keywords = {deep inference},
	pages = {136--153},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {A Quasipolynomial Cut-Elimination Procedure in Deep Inference Via Atomic Flows and Threshold Formulae},
	url = {https://people.bath.ac.uk/ag248/p/QPNDI.pdf},
	volume = {6355},
	year = {2010},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/QPNDI.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-17511-4%5C_9}}

@misc{BrusGugl:09:On-Analy:kx,
	author = {Bruscoli, Paola and Guglielmi, Alessio},
	date-added = {2009-11-23 23:46:58 +0100},
	date-modified = {2014-05-08 14:34:37 +0000},
	keywords = {deep inference},
	title = {On Analyticity in Deep Inference},
	url = {https://people.bath.ac.uk/ag248/p/ADI.pdf},
	year = {2009},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/ADI.pdf}}

@article{BrusGugl:07:On-the-P:fk,
	author = {Bruscoli, Paola and Guglielmi, Alessio},
	date-added = {2007-08-25 21:18:04 +0100},
	date-modified = {2014-04-12 10:54:05 +0000},
	doi = {10.1145/1462179.1462186},
	journal = {ACM Transactions on Computational Logic},
	keywords = {deep inference},
	number = {2},
	pages = {14:1--34},
	title = {On the Proof Complexity of Deep Inference},
	url = {https://people.bath.ac.uk/ag248/p/PrComplDI.pdf},
	volume = {10},
	year = {2009},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/PrComplDI.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1145/1462179.1462186}}

@misc{BrusGugl:07:On-Analy:uq,
	author = {Bruscoli, Paola and Guglielmi, Alessio},
	date-added = {2007-09-22 14:54:48 +0100},
	date-modified = {2014-05-08 14:34:58 +0000},
	keywords = {deep inference},
	title = {On Analytic Inference Rules in the Calculus of Structures},
	url = {https://people.bath.ac.uk/ag248/p/Onan.pdf},
	year = {2007},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/Onan.pdf}}

@inproceedings{Brus:02:A-Purely:wd,
	author = {Bruscoli, Paola},
	booktitle = {Logic Programming, 18th International Conference (ICLP)},
	date-modified = {2014-04-11 12:25:06 +0000},
	doi = {10.1007/3-540-45619-8\_21},
	editor = {Peter J. Stuckey},
	keywords = {deep inference},
	pages = {302--316},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {A Purely Logical Account of Sequentiality in Proof Search},
	url = {http://cs.bath.ac.uk/pb/bvl/bvl.pdf},
	volume = {2401},
	year = {2002},
	bdsk-url-1 = {http://cs.bath.ac.uk/pb/bvl/bvl.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/3-540-45619-8%5C_21}}

@inproceedings{Brus:02:A-purely:nx,
	author = {Bruscoli, Paola},
	booktitle = {17. WLP: Workshop Logische Programmierung, {TU} {D}resden, {D}ecember 11--13, 2002},
	date-modified = {2014-05-08 15:09:53 +0000},
	editor = {Bertram Fronhöfer and Steffen Hölldobler},
	keywords = {deep inference},
	note = {ISSN 1430--211X},
	number = {TUD--FI03--03},
	organization = {TU Dresden, 01062 Dresden},
	pages = {97--101},
	publisher = {Technische Universität Dresden},
	series = {Technische Berichte der Fakultät Informatik},
	title = {A Purely Logical Account of Sequentiality in Proof Search -- Extended Abstract},
	year = {2002}}

@article{BrunStud:12:Syntacti:fk,
	author = {Brünnler, Kai and Studer, Thomas},
	date-added = {2013-04-23 17:43:44 +0100},
	date-modified = {2016-12-31 18:02:56 +0000},
	doi = {10.1016/j.apal.2012.04.006},
	journal = {Annals of Pure and Applied Logic},
	keywords = {deep inference},
	number = {12},
	pages = {1838---1853},
	title = {Syntactic Cut-Elimination for a Fragment of the Modal Mu-Calculus},
	url = {http://www.iam.unibe.ch/ltgpub/2012/bs12.pdf},
	volume = {163},
	year = {2012},
	bdsk-url-1 = {http://www.iam.unibe.ch/ltgpub/2012/bs12.pdf}}

@inproceedings{BrunGoetKuzn:10:A-Syntac:uq,
	author = {Brünnler, Kai and Goetschi, Remo and Kuznets, Roman},
	booktitle = {Advances in Modal Logic (AiML)},
	date-added = {2010-11-28 17:17:19 +0000},
	date-modified = {2014-04-26 17:06:13 +0000},
	editor = {Lev Beklemishev and Valentin Goranko and Valentin Shehtman},
	keywords = {deep inference},
	pages = {39--58},
	publisher = {College Publications},
	title = {A Syntactic Realization Theorem for Justification Logics},
	url = {https://people.bath.ac.uk/ag248/kai/2010srtjl.pdf},
	volume = {8},
	year = {2010},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/2010srtjl.pdf}}

@inproceedings{Brun:10:How-to-U:kx,
	author = {Brünnler, Kai},
	booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17)},
	date-added = {2010-11-28 17:53:20 +0000},
	date-modified = {2016-12-31 10:10:05 +0000},
	doi = {10.1007/978-3-642-16242-8\_13},
	editor = {Fermüller, Christian G. and Voronkov, Andrei},
	keywords = {deep inference},
	pages = {172--186},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {How to Universally Close the Existential Rule},
	url = {https://people.bath.ac.uk/ag248/kai/2010hucer.pdf},
	volume = {6397},
	year = {2010},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/2010hucer.pdf}}

@unpublished{Brun:10:Nested-S:fk,
	author = {Brünnler, Kai},
	date-added = {2010-04-13 18:27:25 +0200},
	date-modified = {2016-06-13 05:46:22 +0000},
	keywords = {deep inference},
	note = {Habilitation Thesis},
	school = {Universität Bern},
	title = {Nested Sequents},
	url = {http://arxiv.org/pdf/1004.1845.pdf},
	year = {2010},
	bdsk-url-1 = {http://arxiv.org/pdf/1004.1845}}

@article{Brun:07:Deep-Seq:fk,
	author = {Brünnler, Kai},
	date-added = {2007-08-26 10:54:46 +0100},
	date-modified = {2016-12-31 18:08:08 +0000},
	doi = {10.1007/s00153-009-0137-3},
	journal = {Archive for Mathematical Logic},
	keywords = {deep inference},
	number = {6},
	pages = {551--577},
	title = {Deep Sequent Systems for Modal Logic},
	url = {https://people.bath.ac.uk/ag248/kai/2009dssml.pdf},
	volume = {48},
	year = {2009},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/2009dssml.pdf}}

@inproceedings{BrunStra:09:Modular-:ys,
	author = {Brünnler, Kai and Straßburger, Lutz},
	booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux)},
	date-added = {2009-05-08 16:15:49 +0200},
	date-modified = {2016-12-31 18:51:34 +0000},
	doi = {10.1007/978-3-642-02716-1\_12},
	keywords = {deep inference},
	pages = {152--166},
	publisher = {Springer},
	series = {Lecture Notes in Artificial Intelligence},
	title = {Modular Sequent Systems for Modal Logic},
	url = {https://people.bath.ac.uk/ag248/kai/2009mssml.pdf},
	volume = {5607},
	year = {2009},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/2009mssml.pdf}}

@article{BrunStud:09:Syntacti:yq,
	author = {Brünnler, Kai and Studer, Thomas},
	date-added = {2009-05-06 13:13:02 +0200},
	date-modified = {2016-12-31 18:02:54 +0000},
	doi = {10.1016/j.apal.2009.01.014},
	journal = {Annals of Pure and Applied Logic},
	keywords = {deep inference},
	number = {1},
	pages = {82--95},
	title = {Syntactic Cut-Elimination for Common Knowledge},
	url = {https://people.bath.ac.uk/ag248/kai/infck.pdf},
	volume = {160},
	year = {2009},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/infck.pdf}}

@inproceedings{BrunStud::Syntacti:vn,
	author = {Brünnler, Kai and Studer, Thomas},
	booktitle = {5th Workshop on Methods for Modalities (M4M5 2007)},
	date-added = {2007-12-02 20:59:00 +0000},
	date-modified = {2009-03-22 15:51:11 +0100},
	editor = {Areces, Carlos and Demri, Stéphane},
	keywords = {deep inference},
	pages = {227--240},
	publisher = {Elsevier},
	series = {Electronic Notes in Theoretical Computer Science},
	title = {Syntactic Cut-Elimination for Common Knowledge},
	url = {https://people.bath.ac.uk/ag248/kai/m4m5.pdf},
	volume = {231},
	year = {2009},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/m4m5.pdf}}

@inproceedings{BrunMcKi:08:An-Algor:wq,
	author = {Brünnler, Kai and McKinley, Richard},
	booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)},
	date-added = {2008-07-01 12:05:07 +0100},
	date-modified = {2016-12-31 10:11:06 +0000},
	doi = {10.1007/978-3-540-89439-1\_34},
	editor = {Cervesato, Iliano and Veith, Helmut and Voronkov, Andrei},
	keywords = {deep inference},
	pages = {482---496},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {An Algorithmic Interpretation of a Deep Inference System},
	url = {https://people.bath.ac.uk/ag248/kai/2008aidis.pdf},
	volume = {5330},
	year = {2008},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/2008aidis.pdf}}

@article{Brun:06:Cut-Elim:cq,
	author = {Brünnler, Kai},
	date-modified = {2015-07-28 06:35:53 +0000},
	doi = {10.1007/s11225-006-6605-4},
	journal = {Studia Logica},
	keywords = {deep inference},
	number = {1},
	pages = {51--71},
	title = {Cut Elimination Inside a Deep Inference System for Classical Predicate Logic},
	url = {https://people.bath.ac.uk/ag248/kai/q.pdf},
	volume = {82},
	year = {2006},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/q.pdf}}

@inproceedings{Brun:06:Deep-Inf:qy,
	author = {Brünnler, Kai},
	booktitle = {Logical Approaches to Computational Barriers---2nd Conference on Computability in Europe},
	date-added = {2006-07-16 14:57:44 +0100},
	date-modified = {2016-12-31 10:10:25 +0000},
	doi = {10.1007/11780342\_7},
	editor = {Beckmann, Arnold and Berger, Ulrich and Löwe, Benedikt and Tucker, John V.},
	keywords = {deep inference},
	pages = {65--74},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Deep Inference and Its Normal Form of Derivations},
	url = {https://people.bath.ac.uk/ag248/kai/n.pdf},
	volume = {3988},
	year = {2006},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/n.pdf}}

@inproceedings{Brun::Deep-Seq:ay,
	author = {Brünnler, Kai},
	booktitle = {Advances in Modal Logic (AiML)},
	date-added = {2006-03-30 17:44:13 +0100},
	date-modified = {2014-04-26 17:06:13 +0000},
	editor = {Guido Governatori and Ian Hodkinson and Yde Venema},
	keywords = {deep inference},
	pages = {107--119},
	publisher = {College Publications},
	title = {Deep Sequent Systems for Modal Logic},
	url = {http://www.aiml.net/volumes/volume6/Bruennler.ps},
	volume = {6},
	year = {2006},
	bdsk-url-1 = {http://www.aiml.net/volumes/volume6/Bruennler.ps}}

@article{Brun:06:Locality:zh,
	author = {Brünnler, Kai},
	date-modified = {2015-06-08 11:01:59 +0000},
	doi = {10.1305/ndjfl/1168352668},
	journal = {Notre Dame Journal of Formal Logic},
	keywords = {deep inference},
	number = {4},
	pages = {557--580},
	title = {Locality for Classical Logic},
	url = {https://people.bath.ac.uk/ag248/kai/LocalityClassical.pdf},
	volume = {47},
	year = {2006},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/LocalityClassical.pdf}}

@inproceedings{BrunLeng:05:On-Two-F:jf,
	author = {Brünnler, Kai and Lengrand, Stéphane},
	booktitle = {Structures and Deduction},
	date-modified = {2006-12-24 12:12:26 +0000},
	editor = {Paola Bruscoli and François Lamarche and Charles Stewart},
	keywords = {deep inference},
	note = {ICALP Workshop. ISSN 1430-211X},
	pages = {69--80},
	publisher = {Technische Universität Dresden},
	title = {On Two Forms of Bureaucracy in Derivations},
	url = {https://people.bath.ac.uk/ag248/kai/sd05.pdf},
	year = {2005},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/sd05.pdf}}

@incollection{BrunGugl:04:A-First-:ys,
	author = {Brünnler, Kai and Guglielmi, Alessio},
	booktitle = {First-Order Logic Revisited},
	city = {Berlin},
	date-modified = {2013-03-17 17:21:34 +0000},
	editor = {Hendricks, Vincent and Neuhaus, Fabian and Pedersen, Stig Andur and Scheffler, Uwe and Wansing, Heinrich},
	keywords = {deep inference},
	pages = {59--74},
	publisher = {Logos Verlag},
	series = {Logische Philosophie},
	title = {A First Order System with Finite Choice of Premises},
	url = {https://people.bath.ac.uk/ag248/kai/FinFOL.pdf},
	year = {2004},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/FinFOL.pdf}}

@book{Brun:04:Deep-Inf:rq,
	address = {Berlin},
	author = {Brünnler, Kai},
	date-modified = {2006-07-13 13:12:55 +0100},
	keywords = {deep inference},
	publisher = {Logos Verlag},
	title = {Deep Inference and Symmetry in Classical Proofs},
	url = {https://people.bath.ac.uk/ag248/kai/phd.pdf},
	year = {2004},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/phd.pdf}}

@inproceedings{Brun:03:Atomic-C:oz,
	author = {Brünnler, Kai},
	booktitle = {Computer Science Logic (CSL)},
	date-modified = {2016-12-31 10:10:46 +0000},
	doi = {10.1007/978-3-540-45220-1\_9},
	editor = {M. Baaz and J. A. Makowsky},
	keywords = {deep inference},
	pages = {86--97},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Atomic Cut Elimination for Classical Logic},
	url = {https://people.bath.ac.uk/ag248/kai/ace.pdf},
	volume = {2803},
	year = {2003},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/ace.pdf}}

@article{Brun:03:Two-Rest:mn,
	author = {Brünnler, Kai},
	date-modified = {2021-12-23 16:46:30 +0000},
	doi = {10.1093/jigpal/11.5.525},
	journal = {Logic Journal of the {IGPL}},
	keywords = {deep inference},
	number = {5},
	pages = {525--529},
	title = {Two Restrictions on Contraction},
	url = {https://people.bath.ac.uk/ag248/kai/RestContr.pdf},
	volume = {11},
	year = {2003},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/RestContr.pdf}}

@techreport{BrunGugl:02:Consiste:kn,
	author = {Brünnler, Kai and Guglielmi, Alessio},
	date-modified = {2006-07-13 13:12:55 +0100},
	institution = {Technische Universität Dresden},
	keywords = {deep inference},
	number = {WV-02-16},
	title = {Consistency Without Cut Elimination},
	url = {https://people.bath.ac.uk/ag248/p/AG4.pdf},
	year = {2002},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG4.pdf}}

@inproceedings{BrunTiu:01:A-Local-:mz,
	author = {Brünnler, Kai and Tiu, Alwen Fernanto},
	booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)},
	date-modified = {2014-05-20 03:32:27 +0000},
	doi = {10.1007/3-540-45653-8\_24},
	editor = {R. Nieuwenhuis and Voronkov, Andrei},
	keywords = {deep inference},
	pages = {347--361},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {A Local System for Classical Logic},
	url = {https://people.bath.ac.uk/ag248/kai/lcl-lpar.pdf},
	volume = {2250},
	year = {2001},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/kai/lcl-lpar.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/3-540-45653-8%5C_24}}

@techreport{BrunTiu:01:A-Local-:ly,
	author = {Brünnler, Kai and Tiu, Alwen Fernanto},
	date-modified = {2014-04-15 09:32:52 +0000},
	institution = {Technische Universität Dresden},
	keywords = {deep inference},
	number = {WV-01-02},
	title = {A Local System for Classical Logic},
	year = {2001},
	bdsk-url-1 = {http://iccl.tu-dresden.de/~kai/LocalClassicalLogic-tr.pdf}}

@inproceedings{ChauMariStra:16:Modular-:fk,
	author = {Chaudhuri, Kaustuv and Marin, Sonia and Straßburger, Lutz},
	booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD)},
	date-added = {2016-05-02 11:12:58 +0000},
	date-modified = {2016-12-31 19:51:02 +0000},
	doi = {10.4230/LIPIcs.FSCD.2016.16},
	editor = {Kesner, Delia and Pientka, Brigitte},
	keywords = {deep inference},
	pages = {16:1--18},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {Modular Focused Proof Systems for Intuitionistic Modal Logics},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/fscd16focint.pdf},
	volume = {52},
	year = {2016},
	bdsk-url-1 = {http://kaustuv.chaudhuri.info/papers/fossacs16focnest.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-662-49630-5%5C_23}}

@inproceedings{ChauMariStra:16:Focused-:uk,
	author = {Chaudhuri, Kaustuv and Marin, Sonia and Straßburger, Lutz},
	booktitle = {Foundations of Software Science and Computation Structures (FoSSaCS)},
	date-added = {2016-04-13 09:55:11 +0000},
	date-modified = {2016-04-13 09:58:01 +0000},
	doi = {10.1007/978-3-662-49630-5\_23},
	editor = {Jacobs, Bart and Löding, Christof},
	keywords = {deep inference},
	pages = {390--407},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Focused and Synthetic Nested Sequents},
	url = {http://kaustuv.chaudhuri.info/papers/fossacs16focnest.pdf},
	volume = {9634},
	year = {2016},
	bdsk-url-1 = {http://kaustuv.chaudhuri.info/papers/fossacs16focnest.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-662-49630-5%5C_23}}

@inproceedings{ChauGuen:14:Equality:rt,
	author = {Chaudhuri, Kaustuv and Guenot, Nicolas},
	booktitle = {Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
	date-added = {2014-04-26 14:14:04 +0000},
	date-modified = {2015-04-13 08:26:24 +0000},
	doi = {10.1145/2603088.2603140},
	editor = {Henzinger, Thomas and Miller, Dale},
	keywords = {deep inference},
	pages = {30:1--10},
	publisher = {ACM},
	title = {Equality and Fixpoints in the Calculus of Structures},
	url = {http://chaudhuri.info/papers/csllics14eqfix.pdf},
	year = {2014},
	bdsk-url-1 = {http://chaudhuri.info/papers/csllics14eqfix.pdf}}

@inproceedings{ChauGuenStra:11:The-Focu:fk,
	author = {Chaudhuri, Kaustuv and Guenot, Nicolas and Straßburger, Lutz},
	booktitle = {Computer Science Logic (CSL)},
	date-added = {2012-07-07 12:52:40 +0100},
	date-modified = {2014-04-12 11:05:02 +0000},
	doi = {10.4230/LIPIcs.CSL.2011.159},
	editor = {Bezem, Marc},
	keywords = {deep inference},
	pages = {159--173},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {The Focused Calculus of Structures},
	url = {http://drops.dagstuhl.de/opus/volltexte/2011/3229/},
	volume = {12},
	year = {2011},
	bdsk-url-1 = {http://drops.dagstuhl.de/opus/volltexte/2011/3229/pdf/16.pdf},
	bdsk-url-2 = {http://drops.dagstuhl.de/opus/volltexte/2011/3229/},
	bdsk-url-3 = {http://dx.doi.org/10.4230/LIPIcs.CSL.2011.159}}

@inproceedings{CiobHorn:15:Behaviou:ye,
	author = {Ciobanu, Gabriel and Horne, Ross},
	booktitle = {Perspectives of System Informatics (PSI)},
	date-added = {2016-06-30 13:04:02 +0000},
	date-modified = {2019-04-04 18:04:58 +0100},
	doi = {10.1007/978-3-319-41579-6\_8},
	editor = {Mazzara, Manuel and Voronkov, Andrei},
	keywords = {deep inference},
	pages = {91--106},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Behavioural Analysis of Sessions Using the Calculus of Structures},
	url = {http://satoss.uni.lu/members/ross/pdf/sessions.pdf},
	volume = {9609},
	year = {2015},
	bdsk-url-1 = {http://www.ntu.edu.sg/home/rhorne/psi.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-319-41579-6%5C_8}}

@inproceedings{ClouDawsGoreTiu:13:Annotati:sy,
	author = {Clouston, Ranald and Dawson, Jeremy and Goré, Rajeev and Tiu, Alwen},
	booktitle = {Computer Science Logic (CSL)},
	date-added = {2014-04-26 16:39:15 +0000},
	date-modified = {2014-04-26 16:45:01 +0000},
	doi = {10.4230/LIPIcs.CSL.2013.197},
	editor = {Ronchi Della Rocca, Simona},
	keywords = {deep inference},
	note = {Extended version at \url{http://arxiv.org/abs/1307.0289}},
	pages = {197--214},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic},
	volume = {23},
	year = {2013},
	bdsk-url-1 = {http://dx.doi.org/10.4230/LIPIcs.CSL.2013.197}}

@inproceedings{DasRice:21:New-Mini:wt,
	author = {Das, Anupam and Rice, Alex A.},
	booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD)},
	date-added = {2021-12-23 15:49:36 +0000},
	date-modified = {2021-12-23 15:53:10 +0000},
	doi = {10.4230/LIPIcs.FSCD.2021.14},
	editor = {Kobayashi, Naoki},
	keywords = {deep inference},
	pages = {14:1--14:19},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial},
	url = {https://drops.dagstuhl.de/opus/volltexte/2021/14252/pdf/LIPIcs-FSCD-2021-14.pdf},
	volume = {195},
	year = {2021},
	bdsk-url-1 = {https://drops.dagstuhl.de/opus/volltexte/2021/14252/pdf/LIPIcs-FSCD-2021-14.pdf},
	bdsk-url-2 = {https://doi.org/10.4230/LIPIcs.FSCD.2021.14}}

@misc{Das:17:An-Unavo:ty,
	author = {Das, Anupam},
	date-added = {2017-06-24 21:53:36 +0000},
	date-modified = {2017-06-24 21:55:56 +0000},
	keywords = {deep inference},
	title = {An Unavoidable Contraction Loop in Monotone Deep Inference},
	url = {https://people.bath.ac.uk/ag248/das/con-loop.pdf},
	year = {2017},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/das/con-loop.pdf}}

@article{DasStra:16:On-Linea:uk,
	author = {Das, Anupam and Straßburger, Lutz},
	date-added = {2017-02-28 06:35:00 +0000},
	date-modified = {2017-02-28 06:45:22 +0000},
	doi = {10.2168/LMCS-12(4:9)2016},
	journal = {Logical Methods in Computer Science},
	keywords = {deep inference},
	number = {4},
	pages = {9:1--27},
	title = {On Linear Rewriting Systems for Boolean Logic and Some Applications to Proof Theory},
	url = {https://arxiv.org/pdf/1610.08772.pdf},
	volume = {12},
	year = {2016},
	bdsk-url-1 = {https://arxiv.org/pdf/1610.08772.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.2168/LMCS-12(4:9)2016}}

@inproceedings{Das:16:From-Pos:vn,
	author = {Das, Anupam},
	booktitle = {31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
	date-added = {2016-04-13 08:28:33 +0000},
	date-modified = {2020-12-09 20:06:03 +0000},
	doi = {10.1145/2933575.2934570},
	editor = {Shankar, Natarajan},
	keywords = {deep inference},
	pages = {126--135},
	publisher = {ACM},
	title = {From Positive and Intuitionistic Bounded Arithmetic to Monotone Proof Complexity},
	url = {http://www.anupamdas.com/items/pos-int-bdarith-mon-pc/pos-int-bdarith-mon-pc.pdf},
	year = {2016},
	bdsk-url-1 = {http://www.anupamdas.com/items/pos-int-bdarith-mon-pc/pos-int-bdarith-mon-pc.pdf}}

@inproceedings{DasStra:15:No-Compl:yg,
	author = {Das, Anupam and Straßburger, Lutz},
	booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA)},
	date-added = {2015-04-13 06:50:56 +0000},
	date-modified = {2016-04-13 10:23:08 +0000},
	doi = {10.4230/LIPIcs.RTA.2015.127},
	editor = {Fernández, Maribel},
	keywords = {deep inference},
	pages = {127--142},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {No Complete Linear Term Rewriting System for Propositional Logic},
	url = {http://drops.dagstuhl.de/opus/volltexte/2015/5193/pdf/13.pdf},
	volume = {36},
	year = {2015},
	bdsk-url-1 = {http://www.anupamdas.com/items/NoCompLinSys/NoCompLinSys.pdf}}

@article{Das:13:Some-Res:fk,
	author = {Das, Anupam},
	date-added = {2013-04-06 17:28:37 +0100},
	date-modified = {2015-04-13 09:25:38 +0000},
	doi = {10.2168/LMCS-11(1:4)2015},
	journal = {Logical Methods in Computer Science},
	keywords = {deep inference},
	number = {1},
	pages = {4:1--27},
	title = {On the Relative Proof Complexity of Deep Inference Via Atomic Flows},
	url = {http://arxiv.org/pdf/1502.05860.pdf},
	volume = {11},
	year = {2015},
	bdsk-url-1 = {http://www.anupamdas.com/items/RelCompFull/RelCompFull.pdf}}

@phdthesis{Das:14:The-Comp:eu,
	author = {Das, Anupam},
	date-added = {2016-04-13 08:36:10 +0000},
	date-modified = {2016-04-13 08:37:27 +0000},
	keywords = {deep inference},
	school = {University of Bath},
	title = {The Complexity of Propositional Proofs in Deep Inference},
	url = {http://www.anupamdas.com/items/thesis/Thesis-AnupamDas.pdf},
	year = {2014},
	bdsk-url-1 = {http://www.anupamdas.com/items/thesis/Thesis-AnupamDas.pdf}}

@inproceedings{Das:13:The-Pige:fk,
	author = {Das, Anupam},
	booktitle = {Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
	date-added = {2013-03-05 20:50:34 +0000},
	date-modified = {2015-04-13 08:28:14 +0000},
	doi = {10.1145/2603088.2603164},
	editor = {Henzinger, Thomas and Miller, Dale},
	keywords = {deep inference},
	pages = {36:1--10},
	publisher = {ACM},
	title = {On the Pigeonhole and Related Principles in Deep Inference and Monotone Systems},
	url = {http://www.anupamdas.com/items/WeakMonProofsPHP/WeakMonProofsPHP.pdf},
	year = {2014},
	bdsk-url-1 = {http://www.anupamdas.com/items/WeakMonProofsPHP/WeakMonProofsPHP.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1145/2603088.2603164}}

@inproceedings{Das:13:Rewritin:uq,
	author = {Das, Anupam},
	booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA)},
	date-added = {2013-03-05 20:52:11 +0000},
	date-modified = {2014-04-26 16:27:15 +0000},
	doi = {10.4230/LIPIcs.RTA.2013.158},
	editor = {van Raamsdonk, Femke},
	keywords = {deep inference},
	pages = {158--173},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {Rewriting with Linear Inferences in Propositional Logic},
	url = {http://www.anupamdas.com/items/RewritingWithLinearInferences/RewritingWithLinearInferences.pdf},
	volume = {21},
	year = {2013},
	bdsk-url-1 = {http://www.anupamdas.com/items/RewritingWithLinearInferences/RewritingWithLinearInferences.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.4230/LIPIcs.RTA.2013.158}}

@inproceedings{Das:12:Complexi:kx,
	author = {Das, Anupam},
	booktitle = {Computability in Europe},
	date-added = {2012-07-07 15:09:55 +0100},
	date-modified = {2015-04-13 09:47:13 +0000},
	doi = {10.1007/978-3-642-30870-3\_15},
	editor = {Cooper, S. Barry and Dawar, Anuj and Löwe, Benedikt},
	keywords = {deep inference},
	pages = {139--150},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Complexity of Deep Inference Via Atomic Flows},
	url = {http://www.anupamdas.com/items/RelComp/RelComp.pdf},
	volume = {7318},
	year = {2012},
	bdsk-url-1 = {http://www.anupamdas.com/items/RelComp/RelComp.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-30870-3%5C_15}}

@inproceedings{Das:11:On-the-P:fk,
	author = {Das, Anupam},
	booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux)},
	date-added = {2011-05-04 11:55:58 +0100},
	date-modified = {2016-12-31 18:51:26 +0000},
	doi = {10.1007/978-3-642-22119-4\_12},
	editor = {Brünnler, Kai and Metcalfe, George},
	keywords = {deep inference},
	pages = {134--148},
	publisher = {Springer},
	series = {Lecture Notes in Artificial Intelligence},
	title = {On the Proof Complexity of Cut-Free Bounded Deep Inference},
	url = {http://www.anupamdas.com/items/PrCompII/ProofComplexityBoundedDI.pdf},
	volume = {6793},
	year = {2011},
	bdsk-url-1 = {http://www.anupamdas.com/items/PrCompII/ProofComplexityBoundedDI.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-22119-4%5C_12}}

@inproceedings{Di-G:04:Structur:wy,
	author = {Di Gianantonio, Pietro},
	booktitle = {Computer Science Logic (CSL)},
	date-modified = {2016-06-13 05:31:05 +0000},
	doi = {10.1007/978-3-540-30124-0\_13},
	editor = {J. Marcinkowski and A. Tarlecki},
	keywords = {deep inference},
	pages = {130--144},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Structures for Multiplicative Cyclic Linear Logic: {D}eepness Vs Cyclicity},
	url = {https://users.dimi.uniud.it/~pietro.digianantonio/papers/copy_pdf/smcll.pdf},
	volume = {3210},
	year = {2004},
	bdsk-url-1 = {http://www.dimi.uniud.it/~pietro/papers/Soft-copy-ps/scll.ps.gz}}

@inproceedings{DonaStruWern:22:A-Drag-a:de,
	author = {Donato, Pablo and Strub, Pierre-Yves and Werner, Benjamin},
	booktitle = {11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP)},
	date-added = {2022-11-02 19:39:44 +0000},
	date-modified = {2022-11-02 19:39:44 +0000},
	doi = {10.1145/3497775.3503692},
	editor = {Popescu, Andrei and Zdancewic, Steve},
	keywords = {deep inference},
	pages = {197--209},
	publisher = {ACM},
	title = {A Drag-and-Drop Proof Tactic},
	url = {http://www.lix.polytechnique.fr/Labo/Pablo.DONATO/papers/cpp-article.pdf},
	year = {2022},
	bdsk-url-1 = {https://doi.org/10.1145%2F3497775.3503692},
	bdsk-url-2 = {https://doi.org/10.1145/3497775.3503692}}

@article{DyckSadrTruf:13:Algebra-:fe,
	author = {Dyckhoff, Roy and Sadrzadeh, Mehrnoosh and Truffaut, Julien},
	date-added = {2014-04-26 15:30:34 +0000},
	date-modified = {2016-06-12 10:27:51 +0000},
	doi = {10.1145/2536740.2536742},
	journal = {ACM Transactions on Computational Logic},
	keywords = {deep inference},
	number = {4},
	pages = {34:1--37},
	title = {Algebra, Proof Theory and Applications for an Intuitionistic Logic of Propositions, Actions and Adjoint Modal Operators},
	url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.307.1219&rep=rep1&type=pdf},
	volume = {14},
	year = {2013},
	bdsk-url-1 = {http://tocl.acm.org/accepted/dyckhoff_algebra.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1145/2536740.2536742}}

@article{FittKuzn:15:Modal-In:dw,
	author = {Fitting, Melvin and Kuznets, Roman},
	date-added = {2016-04-13 10:31:20 +0000},
	date-modified = {2016-06-13 06:08:22 +0000},
	doi = {doi:10.1016/j.apal.2014.11.002},
	journal = {Annals of Pure and Applied Logic},
	keywords = {deep inference},
	number = {3},
	pages = {274--305},
	title = {Modal Interpolation Via Nested Sequents},
	url = {https://sites.google.com/site/kuznets/interpolation.pdf?attredirects=1},
	volume = {166},
	year = {2015},
	bdsk-url-1 = {http://is.gd/tp01QD},
	bdsk-url-2 = {http://dx.doi.org/10.1016/j.apal.2014.11.002}}

@article{Fitt:11:Nested-S:kx,
	author = {Fitting, Melvin},
	date-added = {2012-07-05 17:08:40 +0100},
	date-modified = {2016-06-14 04:46:24 +0000},
	doi = {10.1215/00294527-2377869},
	journal = {Notre Dame Journal of Formal Logic},
	keywords = {deep inference},
	number = {1},
	pages = {41--61},
	title = {Nested Sequents for Intuitionistic Logics},
	url = {http://melvinfitting.org/bookspapers/pdf/papers/IntuitionisticNested.pdf},
	volume = {55},
	year = {2014},
	bdsk-url-1 = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/IntuitionisticNested.pdf}}

@article{Fitt:12:Prefixed:fk,
	author = {Fitting, Melvin},
	date-added = {2012-07-05 16:01:17 +0100},
	date-modified = {2016-06-14 04:44:35 +0000},
	doi = {10.1016/j.apal.2011.09.004},
	journal = {Annals of Pure and Applied Logic},
	keywords = {deep inference},
	number = {3},
	pages = {291--313},
	title = {Prefixed Tableaus and Nested Sequents},
	url = {http://melvinfitting.org/bookspapers/pdf/papers/NestedSequentsPostingVersion/PrefixedDeep.pdf},
	volume = {163},
	year = {2012},
	bdsk-url-1 = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/NestedSequentsPostingVersion/PrefixedDeep.pdf}}

@incollection{Fitt:11:Proving-:uq,
	author = {Fitting, Melvin},
	booktitle = {Logic without Frontiers},
	date-added = {2012-07-05 16:48:58 +0100},
	date-modified = {2016-06-14 04:36:08 +0000},
	editor = {Béziau, Jean-Yves and Coniglio, Marcelo Esteban},
	keywords = {deep inference},
	pages = {145--154},
	publisher = {College Publications},
	series = {Tributes},
	title = {Proving Completeness for Nested Sequent Calculi},
	url = {http://www.melvinfitting.org/bookspapers/pdf/papers/Carnielli.pdf},
	volume = {17},
	year = {2011},
	bdsk-url-1 = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/Carnielli.pdf}}

@inproceedings{GimeMose:13:The-Stru:fk,
	author = {Gimenez, Stéphane and Moser, Georg},
	booktitle = {Computer Science Logic (CSL)},
	date-added = {2013-07-07 22:14:45 +0000},
	date-modified = {2014-04-11 17:18:55 +0000},
	doi = {10.4230/LIPIcs.CSL.2013.316},
	editor = {Ronchi Della Rocca, Simona},
	keywords = {deep inference},
	pages = {316--331},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {The Structure of Interaction},
	url = {http://cl-informatik.uibk.ac.at/users/sgimenez/data/articles/soi.pdf},
	volume = {23},
	year = {2013},
	bdsk-url-1 = {http://cl-informatik.uibk.ac.at/users/sgimenez/data/articles/soi.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.4230/LIPIcs.CSL.2013.316}}

@inproceedings{GirlStra:20:MOIN:-A-:qm,
	author = {Girlando, Marianna and Straßburger, Lutz},
	booktitle = {Automated Reasoning -- 10th International Joint Conference (IJCAR)},
	date-added = {2021-02-07 12:02:52 +0000},
	date-modified = {2021-02-07 12:12:13 +0000},
	doi = {10.1007/978-3-030-51054-1\_25},
	editor = {Sofronie-Stokkermans, Viorica and Peltier, Nicolas},
	keywords = {deep inference},
	pages = {398--407},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {{MOIN}: {A} Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)},
	url = {https://hal.inria.fr/hal-02457240v3/document},
	volume = {12166},
	year = {2020},
	bdsk-url-1 = {https://hal.inria.fr/hal-02457240v3/document},
	bdsk-url-2 = {https://doi.org/10.1007/978-3-030-51054-1%5C_25}}

@inproceedings{GoreRama:12:Labelled:fk,
	author = {Goré, Rajeev and Ramanayake, Revantha},
	booktitle = {Advances in Modal Logic (AiML)},
	date-added = {2012-07-08 16:26:52 +0100},
	date-modified = {2016-06-13 06:09:42 +0000},
	editor = {Bolander, Thomas and Braüner, Torben and Ghilardi, Silvio and Lawrence Moss},
	keywords = {deep inference},
	pages = {279--299},
	publisher = {College Publications},
	title = {Labelled Tree sequents, Tree Hypersequents and Nested (Deep) Sequents},
	url = {http://users.cecs.anu.edu.au/~rpg/Publications/AiML2012/gore-ramanayake-aiml12.pdf},
	volume = {9},
	year = {2012},
	bdsk-url-1 = {http://rsise.anu.edu.au/~rpg/Publications/AiML2012/gore-ramanayake-aiml12.pdf}}

@article{GorePostTiu:11:On-the-C:fk,
	author = {Goré, Rajeev and Postniece, Linda and Tiu, Alwen},
	date-added = {2011-05-05 07:11:03 +0100},
	date-modified = {2016-06-13 05:48:18 +0000},
	doi = {10.2168/LMCS-7(2:8)2011},
	journal = {Logical Methods in Computer Science},
	keywords = {deep inference},
	number = {2},
	pages = {8:1--38},
	title = {On the Correspondence Between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics},
	url = {http://arxiv.org/pdf/1103.5286.pdf},
	volume = {7},
	year = {2011},
	bdsk-url-1 = {http://arxiv.org/pdf/1103.5286}}

@inproceedings{GorePostTiu:10:Cut-Elim:vn,
	author = {Goré, Rajeev and Postniece, Linda and Tiu, Alwen},
	booktitle = {Advances in Modal Logic (AiML)},
	date-added = {2010-11-28 18:18:12 +0000},
	date-modified = {2014-04-26 17:06:13 +0000},
	editor = {Lev Beklemishev and Valentin Goranko and Valentin Shehtman},
	keywords = {deep inference},
	pages = {156--177},
	publisher = {College Publications},
	title = {Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic},
	url = {http://www.aiml.net/volumes/volume8/Gore-Postniece-Tiu.pdf},
	volume = {8},
	year = {2010},
	bdsk-url-1 = {http://www.aiml.net/volumes/volume8/Gore-Postniece-Tiu.pdf}}

@inproceedings{GorePostTiu:09:Taming-D:rt,
	author = {Goré, Rajeev and Postniece, Linda and Tiu, Alwen},
	booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux)},
	date-added = {2009-05-08 15:46:50 +0200},
	date-modified = {2016-12-31 18:51:31 +0000},
	doi = {10.1007/978-3-642-02716-1\_15},
	keywords = {deep inference},
	pages = {189--204},
	publisher = {Springer},
	series = {Lecture Notes in Artificial Intelligence},
	title = {Taming Displayed Tense Logics Using Nested Sequents With Deep Inference},
	url = {http://users.cecs.anu.edu.au/~tiu/papers/kt.pdf},
	volume = {5607},
	year = {2009},
	bdsk-url-1 = {http://users.cecs.anu.edu.au/~tiu/papers/kt.pdf}}

@inproceedings{GorePostTiu:08:Cut-Elim:yq,
	author = {Goré, Rajeev and Postniece, Linda and Tiu, Alwen},
	booktitle = {Advances in Modal Logic (AiML)},
	date-added = {2009-05-08 15:19:06 +0200},
	date-modified = {2014-04-26 17:06:13 +0000},
	editor = {Carlos Areces and Robert Goldblatt},
	keywords = {deep inference},
	pages = {43--66},
	publisher = {College Publications},
	title = {Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents},
	url = {http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf},
	volume = {7},
	year = {2008},
	bdsk-url-1 = {http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf}}

@article{GoreTiu:06:Classica:uq,
	author = {Goré, Rajeev and Tiu, Alwen},
	date-added = {2006-09-13 07:31:25 +0100},
	date-modified = {2016-12-31 18:10:45 +0000},
	doi = {10.1093/logcom/exm026},
	journal = {Journal of Logic and Computation},
	keywords = {deep inference},
	number = {4},
	pages = {767--794},
	title = {Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-free Deep Inference Calculi for {S5}},
	url = {http://users.cecs.anu.edu.au/~tiu/papers/cmdl.pdf},
	volume = {17},
	year = {2007},
	bdsk-url-1 = {http://users.cecs.anu.edu.au/~tiu/papers/cmdl.pdf}}

@inproceedings{GuenStra:14:Symmetri:uq,
	author = {Guenot, Nicolas and Straßburger, Lutz},
	booktitle = {Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
	date-added = {2014-04-26 14:04:01 +0000},
	date-modified = {2015-04-13 08:30:11 +0000},
	doi = {10.1145/2603088.2603160},
	editor = {Henzinger, Thomas and Miller, Dale},
	keywords = {deep inference},
	pages = {45:1--10},
	publisher = {ACM},
	title = {Symmetric Normalisation for Intuitionistic Logic},
	url = {http://www.lix.polytechnique.fr/Labo/Lutz.Strassburger/papers/sjs2-final-with-appendix.pdf},
	year = {2014},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/Labo/Lutz.Strassburger/papers/sjs2-final-with-appendix.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1145/2603088.2603160}}

@phdthesis{Guen:13:Nested-D:uq,
	author = {Guenot, Nicolas},
	date-added = {2013-04-23 18:40:26 +0100},
	date-modified = {2014-04-26 14:00:45 +0000},
	keywords = {deep inference},
	school = {École Polytechnique},
	title = {Nested Deduction in Logical Foundations for Computation},
	url = {http://www.itu.dk/people/ngue/pub/thesis.pdf},
	year = {2013},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~nguenot/th/thesis.pdf},
	bdsk-url-2 = {http://www.itu.dk/people/ngue/pub/thesis.pdf}}

@inproceedings{Guen:11:Nested-P:la,
	author = {Guenot, Nicolas},
	booktitle = {13th International ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming (PPDP)},
	date-added = {2014-04-26 14:25:16 +0000},
	date-modified = {2015-04-13 08:18:46 +0000},
	doi = {10.1145/2003476.2003501},
	editor = {Hanus, Michael and Schneider-Kamp, Peter},
	keywords = {deep inference},
	pages = {183--193},
	publisher = {ACM},
	series = {PPDP},
	title = {Nested Proof Search as Reduction in the $\lambda$-calculus},
	url = {http://www.itu.dk/people/ngue/pub/ppdp11.pdf},
	year = {2011},
	bdsk-url-1 = {http://www.itu.dk/people/ngue/pub/ppdp11.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1145/2003476.2003501}}

@inproceedings{Guen:10:Focused-:uq,
	author = {Guenot, Nicolas},
	booktitle = {Technical Communications of the 26th International Conference on Logic Programming},
	date-added = {2011-05-05 09:50:18 +0100},
	date-modified = {2014-04-12 11:03:57 +0000},
	doi = {10.4230/LIPIcs.ICLP.2010.84},
	editor = {Manuel Hermenegildo and Torsten Schaub},
	keywords = {deep inference},
	pages = {84--93},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {Focused Proof Search for Linear Logic in the Calculus of Structures},
	url = {http://drops.dagstuhl.de/opus/volltexte/2010/2586/},
	volume = {7},
	year = {2010},
	bdsk-url-1 = {http://drops.dagstuhl.de/opus/volltexte/2010/2586/pdf/10003.GuenotNicolas.2586.pdf},
	bdsk-url-2 = {http://drops.dagstuhl.de/opus/volltexte/2010/2586/},
	bdsk-url-3 = {http://dx.doi.org/10.4230/LIPIcs.ICLP.2010.84}}

@inproceedings{GiulHeijPaul:21:A-Deep-Q:qr,
	author = {Guerrieri, Giulio and Heijltjes, Willem and Paulus, Joseph W.N.},
	booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL)},
	date-added = {2021-02-07 11:55:44 +0000},
	date-modified = {2021-02-07 11:59:42 +0000},
	doi = {10.4230/LIPIcs.CSL.2021.24},
	editor = {Baier, Christel and Goubault-Larrecq, Jean},
	keywords = {deep inference},
	pages = {24:1--24},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {A Deep Quantitative Type System},
	url = {https://drops.dagstuhl.de/opus/volltexte/2021/13458/},
	volume = {183},
	year = {2021},
	bdsk-url-1 = {https://drops.dagstuhl.de/opus/volltexte/2021/13458/},
	bdsk-url-2 = {https://doi.org/10.4230/LIPIcs.CSL.2021.24}}

@misc{Gugl:23:Deep-Inf:qf,
	author = {Guglielmi, Alessio},
	date-added = {2007-03-03 16:59:08 +0000},
	date-modified = {2023-04-12 16:50:04 +0100},
	howpublished = {Web site at \url{http://alessio.guglielmi.name/res/cos}},
	keywords = {deep inference},
	title = {Deep Inference},
	year = {2023}}

@incollection{Gugl:14:Deep-Inf:fj,
	author = {Guglielmi, Alessio},
	booktitle = {All About Proofs, Proofs for All},
	date-added = {2014-12-02 07:20:51 +0000},
	date-modified = {2015-01-25 13:57:50 +0000},
	editor = {Delahaye, David and Woltzenlogel Paleo, Bruno},
	keywords = {deep inference},
	pages = {164--172},
	publisher = {College Publications},
	series = {Mathematical Logic and Foundations},
	title = {Deep Inference},
	url = {https://people.bath.ac.uk/ag248/p/DI.pdf},
	volume = {55},
	year = {2015},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/DI.pdf}}

@misc{Gugl:14:The-Comm:yu,
	author = {Guglielmi, Alessio},
	date-added = {2014-04-15 08:46:19 +0000},
	date-modified = {2014-05-08 14:38:46 +0000},
	keywords = {deep inference},
	title = {The Commutative/Noncommutative Linear Logic BV},
	url = {https://people.bath.ac.uk/ag248/p/CNLLBV.pdf},
	year = {2014},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/CNLLBV.pdf}}

@misc{Gugl:12:A-Person:yu,
	author = {Guglielmi, Alessio},
	date-added = {2014-05-20 00:45:18 +0000},
	date-modified = {2014-05-20 00:48:09 +0000},
	keywords = {deep inference},
	title = {A Personal Perspective on Deep Inference and Computer Science},
	url = {https://people.bath.ac.uk/ag248/p/DICS.pdf},
	year = {2012},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/DICS.pdf}}

@article{GuglStra:02:A-Non-co:dq,
	author = {Guglielmi, Alessio and Straßburger, Lutz},
	date-modified = {2014-04-11 00:30:07 +0000},
	doi = {10.1017/S096012951100003X},
	journal = {Mathematical Structures in Computer Science},
	keywords = {deep inference},
	number = {3},
	pages = {563--584},
	title = {A System of Interaction and Structure {V}: {T}he Exponentials and Splitting},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/NEL-splitting.pdf},
	volume = {21},
	year = {2011},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/NEL-splitting.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1017/S096012951100003X}}

@inproceedings{GuglGundPari::A-Proof-:fk,
	author = {Guglielmi, Alessio and Gundersen, Tom and Parigot, Michel},
	booktitle = {21st International Conference on Rewriting Techniques and Applications (RTA)},
	date-added = {2010-03-15 22:31:13 +0100},
	date-modified = {2014-04-26 16:27:33 +0000},
	doi = {10.4230/LIPIcs.RTA.2010.135},
	editor = {Lynch, Christopher},
	keywords = {deep inference},
	pages = {135--150},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {A Proof Calculus Which Reduces Syntactic Bureaucracy},
	url = {http://drops.dagstuhl.de/opus/volltexte/2010/2649},
	volume = {6},
	year = {2010},
	bdsk-url-1 = {http://drops.dagstuhl.de/opus/volltexte/2010/2649},
	bdsk-url-2 = {http://dx.doi.org/10.4230/LIPIcs.RTA.2010.135}}

@inproceedings{GuglGundStra::Breaking:uq,
	author = {Guglielmi, Alessio and Gundersen, Tom and Straßburger, Lutz},
	booktitle = {25th Annual IEEE Symposium on Logic in Computer Science (LICS)},
	date-added = {2010-01-25 09:14:10 +0100},
	date-modified = {2014-04-12 10:11:00 +0000},
	doi = {10.1109/LICS.2010.12},
	editor = {Jouannaud, Jean-Pierre},
	keywords = {deep inference},
	pages = {284--293},
	publisher = {IEEE},
	title = {Breaking Paths in Atomic Flows for Classical Logic},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/AFII.pdf},
	year = {2010},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/AFII.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1109/LICS.2010.12}}

@misc{Gugl:09:th.pl:rz,
	author = {Guglielmi, Alessio},
	date-added = {2009-02-25 06:54:03 +0100},
	date-modified = {2014-05-01 19:18:43 +0000},
	keywords = {deep inference},
	note = {Prolog program, available at \url{https://people.bath.ac.uk/ag248/p/th.pl}},
	title = {Th.pl},
	year = {2009},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/th.pl}}

@article{GuglGund:07:Normalis:lr,
	author = {Guglielmi, Alessio and Gundersen, Tom},
	date-added = {2007-03-03 11:45:55 +0000},
	date-modified = {2017-08-13 13:58:09 +0000},
	doi = {10.2168/LMCS-4(1:9)2008},
	journal = {Logical Methods in Computer Science},
	keywords = {deep inference},
	number = {1},
	pages = {9:1--36},
	title = {Normalisation Control in Deep Inference Via Atomic Flows},
	url = {https://lmcs.episciences.org/1081/pdf},
	volume = {4},
	year = {2008},
	bdsk-url-1 = {http://www.lmcs-online.org/ojs/viewarticle.php?id=341},
	bdsk-url-2 = {http://arxiv.org/pdf/0709.1205.pdf},
	bdsk-url-3 = {http://dx.doi.org/10.2168/LMCS-4(1:9)2008}}

@misc{GuglGund:08:Normalis:yu,
	author = {Guglielmi, Alessio and Gundersen, Tom},
	date-added = {2008-02-22 16:16:51 +0000},
	date-modified = {2015-04-13 09:47:03 +0000},
	keywords = {deep inference},
	title = {Normalisation Control in Deep Inference Via Atomic Flows {II}},
	url = {https://people.bath.ac.uk/ag248/p/NormContrDIAtFl2.pdf},
	year = {2008},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/NormContrDIAtFl2.pdf}}

@article{Gugl:06:A-System:kl,
	author = {Guglielmi, Alessio},
	date-modified = {2014-04-10 17:06:14 +0000},
	doi = {10.1145/1182613.1182614},
	journal = {ACM Transactions on Computational Logic},
	keywords = {deep inference},
	number = {1},
	pages = {1:1--64},
	title = {A System of Interaction and Structure},
	url = {https://people.bath.ac.uk/ag248/p/SystIntStr.pdf},
	volume = {8},
	year = {2007},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/SystIntStr.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1145/1182613.1182614}}

@misc{Gugl:07:On-the-P:fk,
	author = {Guglielmi, Alessio},
	date-added = {2007-08-12 09:31:38 +0200},
	date-modified = {2014-05-04 12:15:28 +0000},
	keywords = {deep inference},
	note = {Prolog program, available at https://people.bath.ac.uk/ag248/p/PrComplDI.plg},
	title = {On the Proof Complexity of Deep Inference---{C}onjecture},
	year = {2007},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/PrComplDI.plg}}

@misc{Gugl:06:Deep-Inf:ap,
	author = {Guglielmi, Alessio},
	date-modified = {2014-05-08 14:38:36 +0000},
	keywords = {deep inference},
	title = {Deep Inference and the Calculus of Structures---{P}roject Report},
	url = {https://people.bath.ac.uk/ag248/p/CalcStrPR.pdf},
	year = {2006},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/CalcStrPR.pdf}}

@misc{Gugl:05:Butterfl:mb,
	author = {Guglielmi, Alessio},
	date-modified = {2014-05-08 14:38:21 +0000},
	keywords = {deep inference},
	title = {Butterflies},
	url = {https://people.bath.ac.uk/ag248/p/AG7.pdf},
	year = {2005},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG7.pdf}}

@misc{Gugl:05:Some-New:eh,
	author = {Guglielmi, Alessio},
	date-added = {2006-01-16 10:48:24 +0000},
	date-modified = {2014-04-30 13:36:41 +0000},
	keywords = {deep inference},
	title = {Some News on Subatomic Logic},
	url = {https://people.bath.ac.uk/ag248/p/AG16.pdf},
	year = {2005},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG16.pdf}}

@inproceedings{Gugl:05:The-Prob:nu,
	author = {Guglielmi, Alessio},
	booktitle = {Structures and Deduction},
	date-added = {2006-01-16 10:47:46 +0000},
	date-modified = {2006-07-13 13:12:58 +0100},
	editor = {Paola Bruscoli and François Lamarche and Charles Stewart},
	keywords = {deep inference},
	note = {ICALP Workshop. ISSN 1430-211X},
	pages = {53--68},
	publisher = {Technische Universität Dresden},
	title = {The Problem of Bureaucracy and Identity of Proofs from the Perspective of Deep Inference},
	url = {https://people.bath.ac.uk/ag248/p/AG14.pdf},
	year = {2005},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG14.pdf}}

@misc{Gugl:04:Formalis:am,
	author = {Guglielmi, Alessio},
	date-modified = {2014-05-08 14:37:53 +0000},
	keywords = {deep inference},
	title = {Formalism {A}},
	url = {https://people.bath.ac.uk/ag248/p/AG11.pdf},
	year = {2004},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG11.pdf}}

@misc{Gugl:04:Formalis:ea,
	author = {Guglielmi, Alessio},
	date-added = {2006-01-16 10:48:21 +0000},
	date-modified = {2014-05-08 14:38:00 +0000},
	keywords = {deep inference},
	title = {Formalism {B}},
	url = {https://people.bath.ac.uk/ag248/p/AG13.pdf},
	year = {2004},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG13.pdf}}

@misc{Gugl:04:Polynomi:zi,
	author = {Guglielmi, Alessio},
	date-modified = {2014-05-08 14:38:13 +0000},
	keywords = {deep inference},
	title = {Polynomial Size Deep-Inference Proofs Instead of Exponential Size Shallow-Inference Proofs},
	url = {https://people.bath.ac.uk/ag248/p/AG12.pdf},
	year = {2004},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG12.pdf}}

@misc{Gugl:03:Mismatch:pt,
	author = {Guglielmi, Alessio},
	date-modified = {2014-05-08 14:37:16 +0000},
	keywords = {deep inference},
	title = {Mismatch},
	url = {https://people.bath.ac.uk/ag248/p/AG9.pdf},
	year = {2003},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG9.pdf}}

@misc{Gugl:03:Normalis:tf,
	author = {Guglielmi, Alessio},
	date-modified = {2014-05-08 14:37:28 +0000},
	keywords = {deep inference},
	title = {Normalisation Without Cut Elimination},
	url = {https://people.bath.ac.uk/ag248/p/AG6.pdf},
	year = {2003},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG6.pdf}}

@misc{Gugl:03:Resoluti:ce,
	author = {Guglielmi, Alessio},
	date-modified = {2014-05-08 14:37:40 +0000},
	keywords = {deep inference},
	title = {Resolution in the Calculus of Structures},
	url = {https://people.bath.ac.uk/ag248/p/AG10.pdf},
	year = {2003},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG10.pdf}}

@inproceedings{GuglStra:02:A-Non-co:lq,
	author = {Guglielmi, Alessio and Straßburger, Lutz},
	booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)},
	date-modified = {2014-04-11 00:52:55 +0000},
	doi = {10.1007/3-540-36078-6\_16},
	editor = {Baaz, Matthias and Voronkov, Andrei},
	keywords = {deep inference},
	pages = {231--246},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {A Non-commutative Extension of {MELL}},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/NEL.pdf},
	volume = {2514},
	year = {2002},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/NEL.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/3-540-36078-6%5C_16}}

@misc{Gugl:02:Goodness:ti,
	author = {Guglielmi, Alessio},
	date-modified = {2014-05-08 14:36:49 +0000},
	keywords = {deep inference},
	title = {Goodness, Perfection and Miracles},
	url = {https://people.bath.ac.uk/ag248/p/AG1.pdf},
	year = {2002},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG1.pdf}}

@misc{Gugl:02:On-Lafon:iq,
	author = {Guglielmi, Alessio},
	date-modified = {2014-05-08 14:36:59 +0000},
	keywords = {deep inference},
	title = {On {L}afont's Counterexample},
	url = {https://people.bath.ac.uk/ag248/p/AG5.pdf},
	year = {2002},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG5.pdf}}

@misc{Gugl:02:Recipe:xv,
	author = {Guglielmi, Alessio},
	date-modified = {2014-05-08 14:37:09 +0000},
	keywords = {deep inference},
	title = {Recipe},
	url = {https://people.bath.ac.uk/ag248/p/AG2.pdf},
	year = {2002},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG2.pdf}}

@misc{Gugl:02:Subatomi:oh,
	author = {Guglielmi, Alessio},
	date-modified = {2014-04-30 13:36:57 +0000},
	keywords = {deep inference},
	title = {Subatomic Logic},
	url = {https://people.bath.ac.uk/ag248/p/AG8.pdf},
	year = {2002},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/AG8.pdf}}

@inproceedings{GuglStra:01:Non-comm:rp,
	author = {Guglielmi, Alessio and Straßburger, Lutz},
	booktitle = {Computer Science Logic (CSL)},
	date-modified = {2014-05-20 03:34:19 +0000},
	doi = {10.1007/3-540-44802-0\_5},
	editor = {L. Fribourg},
	keywords = {deep inference},
	pages = {54--68},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Non-commutativity and {MELL} in the Calculus of Structures},
	url = {https://people.bath.ac.uk/ag248/p/NoncMELLCoS.pdf},
	volume = {2142},
	year = {2001},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/p/NoncMELLCoS.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/3-540-44802-0%5C_5}}

@techreport{Gugl:99:A-Calcul:jk,
	author = {Guglielmi, Alessio},
	date-added = {2014-05-06 07:40:59 +0000},
	date-modified = {2014-05-06 07:42:55 +0000},
	institution = {Technische Universität Dresden},
	keywords = {deep inference},
	number = {WV-99-04},
	title = {A Calculus of Order and Interaction},
	year = {1999}}

@article{Guir:06:The-Thre:qt,
	author = {Guiraud, Yves},
	date-modified = {2016-12-31 19:18:19 +0000},
	doi = {10.1016/j.apal.2005.12.012},
	journal = {Annals of Pure and Applied Logic},
	keywords = {deep inference},
	number = {1-2},
	pages = {266--295},
	title = {The Three Dimensions of Proofs},
	url = {https://www.irif.fr/~guiraud/recherche/cos1.pdf},
	volume = {141},
	year = {2006},
	bdsk-url-1 = {http://www.loria.fr/~guiraudy/recherche/cos1.pdf}}

@inproceedings{Guir:05:The-Thre:ja,
	author = {Guiraud, Yves},
	booktitle = {Structures and Deduction},
	date-modified = {2006-07-13 13:12:59 +0100},
	editor = {Paola Bruscoli and François Lamarche and Charles Stewart},
	keywords = {deep inference},
	note = {ICALP Workshop. ISSN 1430-211X},
	pages = {35--52},
	publisher = {Technische Universität Dresden},
	title = {The Three Dimensions of Proofs},
	url = {http://cs.bath.ac.uk/pb/SD05/SD05-Proc.pdf},
	year = {2005},
	bdsk-url-1 = {http://cs.bath.ac.uk/pb/SD05/SD05-Proc.pdf}}

@inproceedings{GundHeijPari:13:A-Proof-:kx,
	author = {Gundersen, Tom and Heijltjes, Willem and Parigot, Michel},
	booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-19)},
	date-added = {2014-04-14 17:14:39 +0000},
	date-modified = {2014-12-04 21:10:10 +0000},
	doi = {10.1007/978-3-642-45221-5\_24},
	editor = {McMillan, Ken and Middeldorp, Aart and Voronkov, Andrei},
	keywords = {deep inference},
	pages = {340--354},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus},
	url = {http://www.cs.bath.ac.uk/~wbh22/pdf/strong-normalisation-atomic-lambda-gundersen-heijltjes-parigot-2013.pdf},
	volume = {8312},
	year = {2013},
	bdsk-url-1 = {http://www.cs.bath.ac.uk/~wbh22/docs/SN_atomic_lambda.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-45221-5%5C_24}}

@inproceedings{GundHeijPari:13:Atomic-L:fk,
	author = {Gundersen, Tom and Heijltjes, Willem and Parigot, Michel},
	booktitle = {28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
	date-added = {2013-03-23 11:39:59 +0000},
	date-modified = {2020-12-09 20:03:27 +0000},
	doi = {10.1109/LICS.2013.37},
	editor = {Kupferman, Orna},
	keywords = {deep inference},
	pages = {311--320},
	publisher = {IEEE},
	title = {Atomic Lambda Calculus: {A} Typed Lambda-Calculus with Explicit Sharing},
	url = {http://opus.bath.ac.uk/34527/1/AL.pdf},
	year = {2013},
	bdsk-url-1 = {http://opus.bath.ac.uk/34527/1/AL.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1109/LICS.2013.37}}

@phdthesis{Gund:09:A-Genera:kx,
	author = {Gundersen, Tom},
	date-added = {2009-08-09 11:17:28 +0200},
	date-modified = {2016-06-13 06:13:51 +0000},
	keywords = {deep inference},
	school = {University of Bath},
	title = {A General View of Normalisation Through Atomic Flows},
	url = {https://tel.archives-ouvertes.fr/file/index/docid/509241/filename/thesis.pdf},
	year = {2009},
	bdsk-url-1 = {http://tel.archives-ouvertes.fr/docs/00/50/92/41/PDF/thesis.pdf}}

@phdthesis{He:18:The-Atom:nx,
	author = {He, Fanny},
	date-added = {2018-07-13 16:46:33 +0000},
	date-modified = {2018-07-13 17:20:52 +0000},
	keywords = {deep inference},
	school = {University of Bath},
	title = {The Atomic Lambda-Mu Calculus},
	url = {https://fh341.github.io/pdf/HE-Thesis.pdf},
	year = {2018},
	bdsk-url-1 = {http://people.bath.ac.uk/fh341/pdf/HE-Thesis.pdf}}

@mastersthesis{Hein:05:Geometri:bs,
	author = {Hein, Robert},
	date-modified = {2006-07-13 13:12:56 +0100},
	keywords = {deep inference},
	school = {Technische Universität Dresden},
	title = {Geometric Theories and Modal Logic in the Calculus of Structures},
	url = {http://bitschnitzer.de/robert_thesis.ps.gz},
	year = {2005},
	bdsk-url-1 = {http://bitschnitzer.de/robert_thesis.ps.gz}}

@inproceedings{HeinStew:05:Purity-T:tg,
	author = {Hein, Robert and Stewart, Charles},
	booktitle = {Structures and Deduction},
	date-modified = {2006-07-13 13:12:58 +0100},
	editor = {Paola Bruscoli and François Lamarche and Charles Stewart},
	keywords = {deep inference},
	note = {ICALP Workshop. ISSN 1430-211X},
	pages = {126--143},
	publisher = {Technische Universität Dresden},
	title = {Purity Through Unravelling},
	url = {http://cs.bath.ac.uk/pb/SD05/SD05-Proc.pdf},
	year = {2005},
	bdsk-url-1 = {http://cs.bath.ac.uk/pb/SD05/SD05-Proc.pdf}}

@inproceedings{Horn:19:The-Sub-:dg,
	author = {Horne, Ross},
	booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD)},
	date-added = {2019-11-10 20:27:47 +0000},
	date-modified = {2019-11-10 20:32:11 +0000},
	doi = {10.4230/LIPIcs.FSCD.2019.23},
	editor = {Geuvers, Herman},
	keywords = {deep inference},
	pages = {23:1--16},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {The Sub-Additives: {A} Proof Theory for Probabilistic Choice Extending Linear Logic},
	url = {http://drops.dagstuhl.de/opus/volltexte/2019/10530/pdf/LIPIcs-FSCD-2019-23.pdf},
	volume = {131},
	year = {2019},
	bdsk-url-1 = {http://drops.dagstuhl.de/opus/volltexte/2019/10530/pdf/LIPIcs-FSCD-2019-23.pdf},
	bdsk-url-2 = {https://doi.org/10.4230/LIPIcs.FSCD.2019.23}}

@article{HornTiuAmanCiob:19:De-Morga:ng,
	author = {Horne, Ross and Tiu, Alwen and Aman, Bogdan and Ciobanu, Gabriel},
	date-added = {2019-11-10 19:46:03 +0000},
	date-modified = {2019-11-10 19:50:11 +0000},
	doi = {10.1145/3325821},
	journal = {ACM Transactions on Computational Logic},
	keywords = {deep inference},
	number = {4},
	pages = {22:1--44},
	title = {De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic},
	volume = {20},
	year = {2019},
	bdsk-url-1 = {https://doi.org/10.1145/3325821}}

@article{HornTiu:19:Construc:ft,
	author = {Horne, Ross and Tiu, Alwen},
	date-added = {2019-04-04 18:33:13 +0100},
	date-modified = {2019-11-10 18:04:42 +0000},
	doi = {10.1017/S0960129518000452},
	journal = {Mathematical Structures in Computer Science},
	keywords = {deep inference},
	number = {8},
	pages = {1275--1308},
	title = {Constructing Weak Simulations from Linear Implications for Processes with Private Names},
	url = {https://satoss.uni.lu/members/ross/pdf/MSCS.pdf},
	volume = {29},
	year = {2019},
	bdsk-url-1 = {https://doi.org/10.1017/S0960129518000452}}

@article{HornMauwTiu:17:Semantic:vh,
	author = {Horne, Ross and Mauw, Sjouke and Tiu, Alwen},
	date-added = {2019-04-04 22:23:35 +0100},
	date-modified = {2019-04-04 22:27:34 +0100},
	doi = {10.3233/FI-2017-1531},
	journal = {Fundamenta Informaticae},
	keywords = {deep inference},
	number = {1-2},
	pages = {57--86},
	title = {Semantics for Specialising Attack Trees based on Linear Logic},
	url = {http://orbilu.uni.lu/bitstream/10993/34365/1/HMT17.pdf},
	volume = {153},
	year = {2017},
	bdsk-url-1 = {http://orbilu.uni.lu/bitstream/10993/34365/1/HMT17.pdf},
	bdsk-url-2 = {https://doi.org/10.3233/FI-2017-1531}}

@inproceedings{HornTiuCiob:16:Private-:ty,
	author = {Horne, Ross and Tiu, Alwen and Aman, Bogdan and Ciobanu, Gabriel},
	booktitle = {27th International Conference on Concurrency Theory (CONCUR)},
	date-added = {2016-06-30 12:45:07 +0000},
	date-modified = {2019-04-04 18:23:16 +0100},
	doi = {10.4230/LIPIcs.CONCUR.2016.31},
	editor = {Desharnais, Josée and Jagadeesan, Radha},
	keywords = {deep inference},
	pages = {31:1--16},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {Private Names in Non-Commutative Logic},
	url = {http://drops.dagstuhl.de/opus/volltexte/2016/6175/pdf/LIPIcs-CONCUR-2016-31.pdf},
	volume = {59},
	year = {2016},
	bdsk-url-1 = {http://www.ntu.edu.sg/home/rhorne/p31-Horne.pdf}}

@article{Horn:15:The-cons:ul,
	author = {Horne, Ross},
	date-added = {2016-06-30 12:55:59 +0000},
	date-modified = {2019-04-04 18:22:38 +0100},
	doi = {10.7561/SACS.2015.2.245},
	journal = {Scientific Annals of Computer Science},
	keywords = {deep inference},
	number = {2},
	pages = {245--316},
	title = {The Consistency and Complexity of {M}ultiplicative {A}dditive {S}ystem {V}irtual},
	url = {http://orbilu.uni.lu/bitstream/10993/37434/1/sacs.pdf},
	volume = {25},
	year = {2015},
	bdsk-url-1 = {http://www.ntu.edu.sg/home/rhorne/sacs.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.7561/SACS.2015.2.245}}

@mastersthesis{Hors:06:The-Logi:fk,
	author = {Horsfall, Benjamin Robert},
	date-added = {2007-09-08 07:07:08 +0100},
	date-modified = {2016-06-17 12:20:49 +0000},
	keywords = {deep inference},
	school = {University of Melbourne},
	title = {The Logic of Bunched Implications: {A} Memoir},
	url = {https://minerva-access.unimelb.edu.au/bitstream/handle/11343/39480/72729_00002633_01_horsfall-mcs.pdf?sequence=1},
	year = {2006},
	bdsk-url-1 = {http://www.cs.mu.oz.au/~horsfall/horsfall-mcs.pdf}}

@inproceedings{HughStraWu:21:Combinat:ja,
	author = {Hughes, Dominic J.D. and Straßburger, Lutz and Wu, Jui-Hsuan},
	booktitle = {36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
	date-added = {2022-11-02 19:39:44 +0000},
	date-modified = {2022-11-02 19:39:44 +0000},
	doi = {10.1109/lics52264.2021.9470579},
	editor = {Libkin, Leonid},
	keywords = {deep inference},
	pages = {1--13},
	publisher = {IEEE},
	title = {Combinatorial Proofs and Decomposition Theorems for First-Order Logic},
	url = {https://hal.inria.fr/hal-03369764/document},
	year = {2021},
	bdsk-url-1 = {https://doi.org/10.1109/lics52264.2021.9470579}}

@misc{Hugh:04:Deep-Inf:fc,
	author = {Hughes, Dominic J.D.},
	date-modified = {2014-05-08 14:39:24 +0000},
	keywords = {deep inference},
	title = {Deep Inference Proof Theory Equals Categorical Proof Theory Minus Coherence},
	url = {http://boole.stanford.edu/~dominic/papers/di/di.pdf},
	year = {2004},
	bdsk-url-1 = {http://boole.stanford.edu/~dominic/papers/di/di.pdf}}

@article{Japa:20:Elementa:ly,
	author = {Japaridze, Giorgi},
	date-added = {2021-12-23 17:06:01 +0000},
	date-modified = {2021-12-23 17:08:54 +0000},
	doi = {10.1093/jigpal/jzaa022},
	journal = {Logic Journal of the {IGPL}},
	keywords = {deep inference},
	number = {5},
	title = {Elementary-Base Cirquent Calculus II: {C}hoice Quantifiers},
	url = {https://arxiv.org/pdf/1902.07123.pdf},
	volume = {29},
	year = {2020},
	bdsk-url-1 = {https://arxiv.org/pdf/1902.07123.pdf},
	bdsk-url-2 = {https://doi.org/10.1093/jigpal/jzaa022}}

@article{Japa:18:Elementa:zo,
	author = {Japaridze, Giorgi},
	date-added = {2020-12-09 20:13:55 +0000},
	date-modified = {2020-12-09 20:20:21 +0000},
	journal = {Journal of Applied Logics},
	keywords = {deep inference},
	number = {1},
	pages = {367--387},
	title = {Elementary-Base Cirquent Calculus I: {P}arallel and Choice Connectives},
	url = {https://arxiv.org/abs/1707.04823},
	volume = {5},
	year = {2018},
	bdsk-url-1 = {https://arxiv.org/abs/1707.04823}}

@article{Japa:07:Cirquent:fk,
	author = {Japaridze, Giorgi},
	date-added = {2007-09-22 14:52:39 +0100},
	date-modified = {2016-06-13 05:50:14 +0000},
	doi = {10.1093/logcom/exn019},
	journal = {Journal of Logic and Computation},
	keywords = {deep inference},
	number = {6},
	pages = {983--1028},
	title = {Cirquent Calculus Deepened},
	url = {http://arxiv.org/pdf/0709.1308.pdf},
	volume = {18},
	year = {2008},
	bdsk-url-1 = {http://arxiv.org/pdf/0709.1308},
	bdsk-url-2 = {http://dx.doi.org/10.1093/logcom/exn019}}

@article{Jera::On-the-C:kx,
	author = {Jeřábek, Emil},
	date-added = {2007-12-02 20:34:04 +0000},
	date-modified = {2016-06-13 06:15:36 +0000},
	doi = {10.1093/logcom/exn054},
	journal = {Journal of Logic and Computation},
	keywords = {deep inference},
	number = {2},
	pages = {323--339},
	title = {Proof Complexity of the Cut-Free Calculus of Structures},
	url = {http://users.math.cas.cz/~jerabek/papers/cos.pdf},
	volume = {19},
	year = {2009},
	bdsk-url-1 = {http://www.math.cas.cz/~jerabek/papers/cos.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1093/logcom/exn054}}

@article{Join:07:Complete:uq,
	author = {Joinet, Jean-Baptiste},
	date-modified = {2016-06-12 10:40:58 +0000},
	doi = {10.2178/jsl/1174668390},
	journal = {Journal of Symbolic Logic},
	keywords = {deep inference},
	number = {1},
	pages = {159--170},
	title = {Completeness of {MLL} Proof-nets w.r.t.\ Weak Distributivity},
	url = {http://www-philo.univ-paris1.fr/Joinet/NEW/PDF/PublicationsVersionOK/10-ok-WeakDistrib.pdf},
	volume = {72},
	year = {2007},
	bdsk-url-1 = {http://www-philo.univ-paris1.fr/Joinet/joinetJSLmain.pdf}}

@inproceedings{Join:05:Complete:os,
	author = {Joinet, Jean-Baptiste},
	booktitle = {Structures and Deduction},
	date-added = {2007-12-02 19:32:51 +0000},
	date-modified = {2007-12-02 19:32:51 +0000},
	editor = {Paola Bruscoli and François Lamarche and Charles Stewart},
	keywords = {deep inference},
	note = {ICALP Workshop. ISSN 1430-211X. Invited talk at WoLLIC '03 under the title `Calculus of Structures and Proof-Nets'},
	pages = {81--94},
	publisher = {Technische Universität Dresden},
	title = {Completeness of {MLL} Proof-nets w.r.t.\ Weak Distributivity},
	url = {http://cs.bath.ac.uk/pb/SD05/SD05-Proc.pdf},
	year = {2005},
	bdsk-url-1 = {http://cs.bath.ac.uk/pb/SD05/SD05-Proc.pdf}}

@unpublished{Kahr::Labelled:ri,
	author = {Kahramanoğulları, Ozan},
	date-modified = {2022-11-02 19:41:03 +0000},
	keywords = {deep inference},
	note = {Presented at the 1st World Congress on Universal Logic},
	title = {Labeled Event Structure Semantics of Linear Logic Planning},
	url = {https://people.bath.ac.uk/ag248/cl/ok/unilog.pdf},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/unilog.pdf}}

@inproceedings{Kahr:17:Deep-Pro:fy,
	author = {Kahramanoğulları, Ozan},
	booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-21)},
	date-added = {2017-05-16 21:31:30 +0000},
	date-modified = {2022-11-02 19:42:38 +0000},
	editor = {Eiter, Thomas and Sands, David},
	keywords = {deep inference},
	pages = {106--124},
	publisher = {EasyChair},
	series = {EPiC Series in Computing},
	title = {Deep Proof Search in {MELL}},
	url = {https://easychair.org/publications/paper/q3S},
	volume = {46},
	year = {2017},
	bdsk-url-1 = {http://easychair.org/publications/download/Deep_Proof_Search_in_MELL}}

@inproceedings{Kahr:16:True-Con:kx,
	author = {Kahramanoğulları, Ozan},
	booktitle = {23rd Workshop on Logic, Language, Information and Computation (WoLLIC)},
	date-added = {2016-05-14 10:01:28 +0000},
	date-modified = {2022-11-02 19:42:35 +0000},
	doi = {10.1007/978-3-662-52921-8\_16},
	editor = {Väänänen, Jouko and Hirvonen, Åsa and de Queiroz, Ruy},
	keywords = {deep inference},
	pages = {249--264},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {True Concurrency of Deep Inference Proofs},
	url = {https://drive.google.com/file/d/0B150TbHH-gFtWVE0dGJMOVFEeTQ/view},
	volume = {9803},
	year = {2016},
	bdsk-url-1 = {https://dl.dropboxusercontent.com/u/34033496/wollic2016.pdf}}

@article{Kahr:08:Interact:ad,
	author = {Kahramanoğulları, Ozan},
	date-added = {2008-07-01 11:53:32 +0100},
	date-modified = {2022-11-02 19:42:32 +0000},
	doi = {10.2168/LMCS-10(2:5)2014},
	journal = {Logical Methods in Computer Science},
	keywords = {deep inference},
	number = {2},
	pages = {5:1--49},
	title = {Interaction and Depth Against Nondeterminism in Proof Search},
	url = {http://arxiv.org/pdf/1403.2628.pdf},
	volume = {10},
	year = {2014},
	bdsk-url-1 = {https://dl.dropbox.com/u/34033496/deep.pdf}}

@article{Kahr:09:On-Linea:ix,
	author = {Kahramanoğulları, Ozan},
	date-added = {2009-01-24 06:35:50 +0100},
	date-modified = {2022-11-02 19:42:29 +0000},
	doi = {10.1016/j.ic.2009.02.008},
	journal = {Information and Computation},
	keywords = {deep inference},
	number = {11},
	pages = {1229--1258},
	publisher = {Elsevier},
	title = {On Linear Logic Planning and Concurrency},
	url = {http://www.sciencedirect.com/science/article/pii/S089054010900073X},
	volume = {207},
	year = {2009},
	bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S089054010900073X}}

@unpublished{Kahr:08:Ingredie:bf,
	author = {Kahramanoğulları, Ozan},
	date-added = {2008-07-01 11:55:42 +0100},
	date-modified = {2022-11-02 19:42:26 +0000},
	keywords = {deep inference},
	note = {Short paper at CL\&C'08},
	title = {Ingredients of a Deep Inference Theorem Prover},
	url = {https://people.bath.ac.uk/ag248/cl/ok/ingredients.pdf},
	year = {2008},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/ingredients.pdf}}

@inproceedings{Kahr:07:Maude-as:lr,
	author = {Kahramanoğulları, Ozan},
	booktitle = {Eighth International Workshop on Rule Based Programming (RULE 2007)},
	date-added = {2007-06-26 09:53:26 +0100},
	date-modified = {2022-11-02 19:42:23 +0000},
	doi = {10.1016/j.entcs.2008.10.033},
	editor = {J. Visser and V. Winter},
	keywords = {deep inference},
	pages = {35--50},
	publisher = {Elsevier},
	series = {Electronic Notes in Theoretical Computer Science},
	title = {Maude as a Platform for Designing and Implementing Deep Inference Systems},
	url = {https://people.bath.ac.uk/ag248/cl/ok/rule07.pdf},
	volume = {219},
	year = {2008},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/rule07.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1016/j.entcs.2008.10.033}}

@inproceedings{Kahr:08:On-Linea:fk,
	author = {Kahramanoğulları, Ozan},
	booktitle = {Language and Automata Theory and Applications},
	date-added = {2008-01-20 08:23:25 +0000},
	date-modified = {2022-11-02 19:42:20 +0000},
	doi = {10.1007/978-3-540-88282-4\_24},
	editor = {Martín-Vide, Carlos and Otto, Friedrich and Fernau, Henning},
	keywords = {deep inference},
	pages = {250--262},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {On Linear Logic Planning and Concurrency},
	url = {https://people.bath.ac.uk/ag248/cl/ok/lata.pdf},
	volume = {5196},
	year = {2008},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/lata.pdf}}

@unpublished{Kahr:04:A-New-Lo:fk,
	author = {Kahramanoğulları, Ozan},
	date-added = {2007-09-08 08:31:48 +0100},
	date-modified = {2022-11-02 19:42:16 +0000},
	keywords = {deep inference},
	note = {Short paper at LPAR 2007},
	title = {On Linear Logic Planning and Concurrency},
	year = {2007}}

@article{Kahr:07:System-B:fk,
	author = {Kahramanoğulları, Ozan},
	date-added = {2007-03-24 13:01:58 +0000},
	date-modified = {2022-11-02 19:42:12 +0000},
	doi = {10.1016/j.apal.2007.11.005},
	journal = {Annals of Pure and Applied Logic},
	keywords = {deep inference},
	number = {1--3},
	pages = {107--121},
	title = {System {BV} Is {NP}-Complete},
	volume = {152},
	year = {2007},
	bdsk-url-1 = {http://dx.doi.org/10.1016/j.apal.2007.11.005}}

@phdthesis{Kahr:06:Nondeter:fk,
	author = {Kahramanoğulları, Ozan},
	date-added = {2007-08-13 18:00:14 +0200},
	date-modified = {2022-11-02 19:42:09 +0000},
	keywords = {deep inference},
	school = {Technische Universität Dresden},
	title = {Nondeterminism and Language Design in Deep Inference},
	url = {https://people.bath.ac.uk/ag248/cl/ok/ozansthesis.pdf},
	year = {2006},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/ozansthesis.pdf}}

@inproceedings{Kahr:06:Reducing:hc,
	author = {Kahramanoğulları, Ozan},
	booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)},
	date-modified = {2022-11-02 19:42:05 +0000},
	doi = {10.1007/11916277\_19},
	editor = {Hermann, Miki and Voronkov, Andrei},
	keywords = {deep inference},
	pages = {272--286},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Reducing Nondeterminism in the Calculus of Structures},
	volume = {4246},
	year = {2006},
	bdsk-url-1 = {http://dx.doi.org/10.1007/11916277%5C_19}}

@inproceedings{Kahr:06:System-B:ht,
	author = {Kahramanoğulları, Ozan},
	booktitle = {12th Workshop on Logic, Language, Information and Computation (WoLLIC)},
	date-modified = {2022-11-02 19:42:02 +0000},
	doi = {10.1016/j.entcs.2005.05.026},
	editor = {de Queiroz, Ruy and Macintyre, Angus and Bittencourt, Guilherme},
	keywords = {deep inference},
	pages = {87--99},
	publisher = {Elsevier},
	series = {Electronic Notes in Theoretical Computer Science},
	title = {System {BV} Is {NP}-Complete},
	url = {https://people.bath.ac.uk/ag248/cl/ok/BVnpc.pdf},
	volume = {143},
	year = {2006},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/BVnpc.pdf}}

@inproceedings{KahrMoreReil:05:Implemen:wb,
	author = {Kahramanoğulları, Ozan and Moreau, Pierre-Etienne and Reilles, Antoine},
	booktitle = {Structures and Deduction},
	date-modified = {2022-11-02 19:41:58 +0000},
	editor = {Paola Bruscoli and François Lamarche and Charles Stewart},
	keywords = {deep inference},
	note = {ICALP Workshop. ISSN 1430-211X},
	pages = {158--172},
	publisher = {Technische Universität Dresden},
	title = {Implementing Deep Inference in {TOM}},
	url = {https://people.bath.ac.uk/ag248/cl/ok/sd05.pdf},
	year = {2005},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/sd05.pdf}}

@inproceedings{Kahr:05:Towards-:uz,
	author = {Kahramanoğulları, Ozan},
	booktitle = {Artificial Intelligence and Applications (AIA)},
	date-modified = {2022-11-02 19:41:49 +0000},
	editor = {Hamza, M.H.},
	keywords = {deep inference},
	pages = {197--202},
	publisher = {ACTA Press},
	title = {Towards Planning as Concurrency},
	url = {https://people.bath.ac.uk/ag248/cl/ok/aia05.pdf},
	year = {2005},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/aia05.pdf}}

@inproceedings{Kahr:04:Implemen:ct,
	address = {Universit\'e Henri Poincar\'e, Nancy, France},
	author = {Kahramanoğulları, Ozan},
	booktitle = {ESSLLI 2004 Student Session},
	date-modified = {2022-11-02 19:41:45 +0000},
	keywords = {deep inference},
	note = {16th European Summer School in Logic, Language and Information},
	pages = {117--127},
	title = {Implementing System {BV} of the Calculus of Structures in {M}aude},
	url = {https://people.bath.ac.uk/ag248/cl/ok/esslli04.pdf},
	year = {2004},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/esslli04.pdf}}

@inproceedings{Kahr:04:System-B:dg,
	author = {Kahramanoğulları, Ozan},
	booktitle = {19th International Symposium on Computer and Information Sciences (ISCIS)},
	date-modified = {2022-11-02 19:41:41 +0000},
	doi = {10.1007/978-3-540-30182-0\_99},
	editor = {C. Aykanat and T. Dayar and I. Körpeoğlu},
	keywords = {deep inference},
	pages = {986--995},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {System {BV} without the Equalities for Unit},
	url = {https://people.bath.ac.uk/ag248/cl/ok/bvn.pdf},
	volume = {3280},
	year = {2004},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/cl/ok/bvn.pdf}}

@article{KuznStra:18:Maehara-:wk,
	author = {Kuznets, Roman and Straßburger, Lutz},
	date-added = {2019-04-04 22:07:38 +0100},
	date-modified = {2019-04-04 22:14:19 +0100},
	doi = {10.1007/s00153-018-0636-1},
	journal = {Archive for Mathematical Logic},
	keywords = {deep inference},
	number = {3-4},
	pages = {359--385},
	title = {Maehara-Style Modal Nested Calculi},
	url = {https://hal.inria.fr/hal-01942240/document},
	volume = {58},
	year = {2018},
	bdsk-url-1 = {https://hal.inria.fr/hal-01942240/document},
	bdsk-url-2 = {https://doi.org/10.1007/s00153-018-0636-1}}

@article{Lama::Explorin:mw,
	author = {Lamarche, François},
	date-added = {2006-06-11 12:09:02 +0100},
	date-modified = {2016-12-31 18:23:41 +0000},
	journal = {Theory and Applications of Categories},
	keywords = {deep inference},
	number = {17},
	pages = {473--535},
	title = {Exploring the Gap between Linear and Classical Logic},
	url = {http://www.tac.mta.ca/tac/volumes/18/17/18-17.pdf},
	volume = {18},
	year = {2007},
	bdsk-url-1 = {http://www.loria.fr/~lamarche/papers/Gap.pdf}}

@article{LamaStra:06:From-Pro:et,
	author = {Lamarche, François and Straßburger, Lutz},
	date-modified = {2016-06-13 05:52:42 +0000},
	doi = {10.2168/LMCS-2(4:3)2006},
	journal = {Logical Methods in Computer Science},
	keywords = {deep inference},
	number = {4},
	pages = {3:1--44},
	title = {From Proof Nets to the Free *-Autonomous Category},
	url = {https://arxiv.org/pdf/cs/0605054.pdf},
	volume = {2},
	year = {2006},
	bdsk-url-1 = {http://arxiv.org/pdf/cs.LO/0605054}}

@inproceedings{LamaStra:05:Construc:qq,
	author = {Lamarche, François and Straßburger, Lutz},
	booktitle = {20th Annual IEEE Symposium on Logic in Computer Science (LICS)},
	date-modified = {2016-12-31 18:40:56 +0000},
	doi = {10.1109/LICS.2005.13},
	editor = {Panangaden, Prakash},
	keywords = {deep inference},
	pages = {209--218},
	publisher = {IEEE},
	title = {Constructing Free Boolean Categories},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/FreeBool-long.pdf},
	year = {2005},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/FreeBool-long.pdf}}

@inproceedings{LamaStra:05:Naming-P:ov,
	author = {Lamarche, François and Straßburger, Lutz},
	booktitle = {Typed Lambda Calculi and Applications (TLCA)},
	date-modified = {2016-12-31 10:09:03 +0000},
	doi = {10.1007/11417170\_19},
	editor = {Paweł Urzyczyn},
	keywords = {deep inference},
	pages = {246--261},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Naming Proofs in Classical Propositional Logic},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/namingproofsCL.pdf},
	volume = {3461},
	year = {2005},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/namingproofsCL.pdf}}

@article{LellPime:19:Modulari:fb,
	author = {Lellmann, Björn and Pimentel, Elaine},
	date-added = {2019-04-04 22:17:27 +0100},
	date-modified = {2019-04-04 22:22:43 +0100},
	doi = {10.1145/3288757},
	journal = {ACM Transactions on Computational Logic},
	keywords = {deep inference},
	number = {2},
	pages = {7:1--46},
	title = {Modularisation of Sequent Calculi for Normal and Non-Normal Modalities},
	url = {https://arxiv.org/pdf/1702.08193.pdf},
	volume = {20},
	year = {2019},
	bdsk-url-1 = {https://arxiv.org/pdf/1702.08193.pdf},
	bdsk-url-2 = {https://doi.org/10.1145/3288757}}

@inproceedings{LellOlarPime:17:A-Unifor:qr,
	author = {Lellmann, Björn and Olarte, Carlos and Pimentel, Elaine},
	booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-21)},
	date-added = {2019-04-04 17:51:05 +0100},
	date-modified = {2019-04-05 12:37:35 +0100},
	doi = {10.29007/93qg},
	editor = {Eiter, Thomas and Sands, David},
	keywords = {deep inference},
	pages = {435--455},
	publisher = {EasyChair},
	series = {EPiC Series in Computing},
	title = {A Uniform Framework for Substructural Logics with Modalities},
	url = {https://easychair.org/publications/paper/d5zT},
	volume = {46},
	year = {2017},
	bdsk-url-1 = {https://easychair.org/publications/paper/d5zT}}

@inproceedings{LellPime:15:Proof-Se:jt,
	author = {Lellmann, Björn and Pimentel, Elaine},
	booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20)},
	date-added = {2016-04-13 09:32:41 +0000},
	date-modified = {2016-12-31 19:13:42 +0000},
	doi = {10.1007/978-3-662-48899-7\_39},
	editor = {Davis, Martin and Fehnker, Ansgar and McIver, Annabelle and Voronkov, Andrei},
	keywords = {deep inference},
	pages = {558--574},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Proof Search in Nested Sequent Calculi},
	url = {https://www.logic.at/staff/lellmann/static/publications/2015/2015LPAR.pdf},
	volume = {9450},
	year = {2015},
	bdsk-url-1 = {https://www.logic.at/staff/lellmann/static/publications/2015/2015LPAR.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-662-48899-7%5C_39}}

@phdthesis{Leng:06:Normalis:uq,
	author = {Lengrand, Stéphane},
	date-added = {2007-10-06 07:11:08 +0100},
	date-modified = {2007-10-06 07:15:24 +0100},
	keywords = {deep inference},
	school = {Université Paris VII - Denis Diderot, University of St Andrews},
	title = {Normalisation \& Equivalence in Proof Theory \& Type Theory},
	url = {http://www.lix.polytechnique.fr/~lengrand/Work/Reports/MyThesis.pdf},
	year = {2006},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lengrand/Work/Reports/MyThesis.pdf}}

@misc{LengBrun:05:Getting-:fk,
	author = {Lengrand, Stéphane and Brünnler, Kai},
	date-added = {2007-10-06 06:46:17 +0100},
	date-modified = {2014-05-08 14:39:43 +0000},
	keywords = {deep inference},
	title = {Getting Formalisms {A} and {B} by Proof-Terms and Typing Systems},
	url = {http://www.lix.polytechnique.fr/~lengrand/Work/Reports/DI.ps},
	year = {2005},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lengrand/Work/Reports/DI.ps}}

@article{Lyon:20:On-the-C:rw,
	author = {Lyon, Tim},
	date-added = {2021-02-07 11:51:22 +0000},
	date-modified = {2021-02-07 11:54:10 +0000},
	doi = {10.1093/logcom/exaa078},
	journal = {Journal of Logic and Computation},
	keywords = {deep inference},
	number = {1},
	pages = {213--265},
	title = {On the Correspondence Between Nested Calculi and Semantic Systems for Intuitionistic Logics},
	url = {https://academic.oup.com/logcom/article-pdf/31/1/213/36178019/exaa078.pdf},
	volume = {31},
	year = {2021},
	bdsk-url-1 = {https://academic.oup.com/logcom/article-pdf/31/1/213/36178019/exaa078.pdf},
	bdsk-url-2 = {https://doi.org/10.1093/logcom/exaa078}}

@inproceedings{LyonTiuGoreClou:20:Syntacti:hb,
	author = {Lyon, Tim and Tiu, Alwen and Goré, Rajeev and Clouston, Ranald},
	booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL)},
	date-added = {2020-12-09 19:42:49 +0000},
	date-modified = {2020-12-09 19:47:32 +0000},
	doi = {10.4230/LIPIcs.CSL.2020.28},
	editor = {Fernández, Maribel and Muscholl, Anca},
	keywords = {deep inference},
	pages = {28:1--55},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents},
	url = {https://drops.dagstuhl.de/opus/volltexte/2020/11671/},
	volume = {152},
	year = {2020},
	bdsk-url-1 = {https://drops.dagstuhl.de/opus/volltexte/2020/11671/},
	bdsk-url-2 = {https://doi.org/10.4230/LIPIcs.CSL.2020.28}}

@inproceedings{Lyon:21:Nested-S:qu,
	author = {Lyon, Tim S.},
	booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux)},
	date-added = {2022-11-02 19:39:44 +0000},
	date-modified = {2022-11-02 19:39:44 +0000},
	doi = {10.1007/978-3-030-86059-2\_24},
	editor = {Das, Anupam and Negri, Sara},
	keywords = {deep inference},
	pages = {409--427},
	publisher = {Springer},
	series = {Lecture Notes in Artificial Intelligence},
	title = {Nested Sequents for Intuitionistic Modal Logics via Structural Refinement},
	url = {https://easychair.org/publications/preprint_download/1Cpt},
	volume = {12842},
	year = {2021},
	bdsk-url-1 = {https://doi.org/10.1007/978-3-030-86059-2_24}}

@inproceedings{MariStra:14:Label-fr:qv,
	author = {Marin, Sonia and Straßburger, Lutz},
	booktitle = {Advances in Modal Logic (AiML)},
	date-added = {2014-06-04 11:02:03 +0000},
	date-modified = {2015-04-13 09:09:40 +0000},
	editor = {Goré, Rajeev and Kooi, Barteld and Kurucz, Agi},
	keywords = {deep inference},
	pages = {387--406},
	publisher = {College Publications},
	title = {Label-free Modular Systems for Classical and Intuitionistic Modal Logics},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/modul-modal.pdf},
	volume = {10},
	year = {2014},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/modul-modal.pdf}}

@phdthesis{Mrm-:06:Categori:ff,
	author = {McKinley, Richard},
	date-added = {2006-03-18 10:08:56 +0000},
	date-modified = {2017-09-17 12:07:49 +0000},
	keywords = {deep inference},
	school = {University of Bath},
	title = {Categorical Models of First Order Classical Proofs},
	url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.60.5125&rep=rep1&type=pdf},
	year = {2006},
	bdsk-url-1 = {http://www.cs.bath.ac.uk/~csprim/thesis.pdf}}

@inproceedings{Mrm-:05:Classica:ye,
	author = {McKinley, Richard},
	booktitle = {Structures and Deduction},
	date-modified = {2017-09-17 12:16:04 +0000},
	editor = {Paola Bruscoli and François Lamarche and Charles Stewart},
	keywords = {deep inference},
	note = {ICALP Workshop. ISSN 1430-211X},
	pages = {19--33},
	publisher = {Technische Universität Dresden},
	title = {Classical Categories and Deep Inference},
	url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.59.3889&rep=rep1&type=pdf},
	year = {2005},
	bdsk-url-1 = {http://www.cs.bath.ac.uk/~csprim/csl05.pdf}}

@inproceedings{NguyStra:22:BV-and-P:fo,
	author = {Nguyễn, Lê Thành Dũng (Tito) and Straßburger, Lutz},
	booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL)},
	date-added = {2022-11-02 19:39:44 +0000},
	date-modified = {2022-11-05 16:01:19 +0000},
	doi = {10.4230/LIPICS.CSL.2022.32},
	editor = {Manea, Florin and Simpson, Alex},
	keywords = {deep inference},
	pages = {32:1--17},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {BV and Pomset Logic Are Not the Same},
	url = {https://drops.dagstuhl.de/opus/volltexte/2022/15752/pdf/LIPIcs-CSL-2022-32.pdf},
	volume = {216},
	year = {2022},
	bdsk-url-1 = {https://drops.dagstuhl.de/opus/volltexte/2022/15752/},
	bdsk-url-2 = {https://doi.org/10.4230/LIPICS.CSL.2022.32}}

@article{NovaStra:13:On-the-P:bs,
	author = {Novaković, Novak and Straßburger, Lutz},
	date-added = {2014-04-26 14:44:29 +0000},
	date-modified = {2015-05-01 09:02:13 +0000},
	doi = {10.1145/2701424},
	journal = {ACM Transactions on Computational Logic},
	keywords = {deep inference},
	number = {3},
	pages = {19:1--20},
	title = {On the Power of Substitution in the Calculus of Structures},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/SubstCoS.pdf},
	volume = {16},
	year = {2015},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/SubstCoS.pdf}}

@inproceedings{OmidStra:22:Combinat:wb,
	author = {Omidvar, Giti and Straßburger, Lutz},
	booktitle = {28th International Workshop on Logic, Language, Information, and Computation (WoLLIC)},
	date-added = {2022-11-02 19:39:44 +0000},
	date-modified = {2022-11-02 19:39:44 +0000},
	doi = {10.1007/978-3-031-15298-6\_9},
	editor = {Ciabattoni, Agata and Pimentel, Elaine and de Queiroz, Ruy J.G.B.},
	keywords = {deep inference},
	pages = {141--157},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Combinatorial Flows as Bicolored Atomic Flows},
	url = {https://www.lix.polytechnique.fr/Labo/Lutz.Strassburger/papers/Combinatorial_Flows.pdf},
	volume = {13468},
	year = {2022},
	bdsk-url-1 = {https://doi.org/10.1007/978-3-031-15298-6_9}}

@inproceedings{PimeRamaLell:19:Sequenti:jx,
	author = {Pimentel, Elaine and Ramanayake, Revantha and Lellmann, Björn},
	booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux)},
	date-added = {2019-11-10 19:51:38 +0000},
	date-modified = {2019-11-10 20:00:56 +0000},
	doi = {10.1007/978-3-030-29026-9\_9},
	editor = {Cerrito, Serenella and Popescu, Andrei},
	keywords = {deep inference},
	pages = {147--165},
	publisher = {Springer},
	series = {Lecture Notes in Artificial Intelligence},
	title = {Sequentialising Nested Systems},
	url = {https://www.logic.at/staff/lellmann/static/publications/2019/2019TABLEAUXSEQ-NES.pdf},
	volume = {11714},
	year = {2019},
	bdsk-url-1 = {https://www.logic.at/staff/lellmann/static/publications/2019/2019TABLEAUXSEQ-NES.pdf},
	bdsk-url-2 = {https://doi.org/10.1007/978-3-030-29026-9%5C_9}}

@phdthesis{Lind:11:Proof-Th:vn,
	author = {Postniece, Linda},
	date-added = {2012-07-07 15:46:35 +0100},
	date-modified = {2012-07-07 15:48:25 +0100},
	keywords = {deep inference},
	school = {The Australian National University},
	title = {Proof Theory and Proof Search of Bi-Intuitionistic and Tense Logic},
	url = {http://users.cecs.anu.edu.au/~linda/thesis.pdf},
	year = {2011},
	bdsk-url-1 = {http://users.cecs.anu.edu.au/~linda/thesis.pdf}}

@inproceedings{Post:09:Deep-Inf:kx,
	author = {Linda Postniece},
	booktitle = {16th Workshop on Logic, Language, Information and Computation (WoLLIC)},
	date-added = {2009-06-12 06:25:08 +0200},
	date-modified = {2016-12-31 10:12:47 +0000},
	doi = {10.1007/978-3-642-02261-6\_26},
	editor = {Ono, Hiroakira and Kanazawa, Makoto and de Queiroz, Ruy},
	keywords = {deep inference},
	pages = {320--334},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Deep Inference in Bi-intuitionistic Logic},
	url = {http://users.cecs.anu.edu.au/~linda/postniece-dbi.pdf},
	volume = {5514},
	year = {2009},
	bdsk-url-1 = {http://users.cecs.anu.edu.au/~linda/postniece-dbi.pdf}}

@article{Ralp:20:Herbrand:sz,
	author = {Ralph, Benjamin},
	date-added = {2020-12-09 20:22:17 +0000},
	date-modified = {2020-12-09 20:28:57 +0000},
	doi = {10.1093/logcom/exaa052},
	journal = {Journal of Logic and Computation},
	keywords = {deep inference},
	number = {8},
	pages = {1711--1742},
	title = {Herbrand Proofs and Expansion Proofs as Decomposed Proofs},
	url = {https://academic.oup.com/logcom/article-pdf/30/8/1711/34673322/exaa052.pdf},
	volume = {30},
	year = {2020},
	bdsk-url-1 = {https://academic.oup.com/logcom/article-pdf/30/8/1711/34673322/exaa052.pdf},
	bdsk-url-2 = {https://doi.org/10.1093/logcom/exaa052}}

@inproceedings{RalpStra:19:Towards-:ix,
	author = {Ralph, Benjamin and Straßburger, Lutz},
	booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux)},
	date-added = {2019-11-10 19:59:15 +0000},
	date-modified = {2019-11-10 20:02:22 +0000},
	doi = {10.1007/978-3-030-29026-9\_15},
	editor = {Cerrito, Serenella and Popescu, Andrei},
	keywords = {deep inference},
	pages = {259--276},
	publisher = {Springer},
	series = {Lecture Notes in Artificial Intelligence},
	title = {Towards a Combinatorial Proof Theory},
	url = {https://people.bath.ac.uk/bdr25/files/CPT.pdf},
	volume = {11714},
	year = {2019},
	bdsk-url-1 = {https://people.bath.ac.uk/bdr25/files/CPT.pdf},
	bdsk-url-2 = {https://doi.org/10.1007/978-3-030-29026-9%5C_15}}

@phdthesis{Ralp:19:Modular-:yq,
	author = {Ralph, Benjamin},
	date-added = {2019-04-03 16:00:09 +0100},
	date-modified = {2019-04-03 16:01:26 +0100},
	keywords = {deep inference},
	school = {University of Bath},
	title = {Modular Normalisation of Classical Proofs},
	url = {https://people.bath.ac.uk/ag248/br/phd.pdf},
	year = {2019},
	bdsk-url-1 = {https://people.bath.ac.uk/ag248/br/phd.pdf}}

@inproceedings{Ralp:18:A-Natura:xe,
	author = {Ralph, Benjamin},
	booktitle = {Logical Foundations of Computer Science (LFCS)},
	date-added = {2017-10-21 07:28:22 +0000},
	date-modified = {2019-04-03 15:34:25 +0100},
	doi = {10.1007/978-3-319-72056-2\_18},
	editor = {Artemov, Sergei and Nerode, Anil},
	keywords = {deep inference},
	pages = {289--308},
	publisher = {Springer International Publishing},
	series = {Lecture Notes in Computer Science},
	title = {A Natural Proof System for Herbrand's Theorem},
	url = {https://people.bath.ac.uk/ag248/br/prfsysht.pdf},
	volume = {10703},
	year = {2018},
	bdsk-url-1 = {http://people.bath.ac.uk/bdr25/files/prfsysht.pdf}}

@inproceedings{Reil:06:Canonica:fe,
	author = {Reilles, Antoine},
	booktitle = {6th International Workshop on Rewriting Logic and Its Applications (WRLA 2006)},
	date-added = {2006-03-28 18:48:42 +0100},
	date-modified = {2016-12-31 18:34:44 +0000},
	doi = {10.1016/j.entcs.2007.06.014},
	keywords = {deep inference},
	pages = {165--179},
	publisher = {Elsevier},
	series = {Electronic Notes in Theoretical Computer Science},
	title = {Canonical Abstract Syntax Trees},
	url = {https://arxiv.org/pdf/cs/0601019.pdf},
	volume = {176},
	year = {2007},
	bdsk-url-1 = {http://arxiv.org/pdf/cs.PL/0601019}}

@incollection{Reto:21:Pomset-L:fv,
	author = {Retoré, Christian},
	booktitle = {Joachim Lambek: {T}he Interplay of Mathematics, Logic, and Linguistics},
	date-added = {2021-12-23 14:14:42 +0000},
	date-modified = {2021-12-23 14:58:26 +0000},
	doi = {10.1007/978-3-030-66545-6\_9},
	editor = {Casadio, Claudia and Scott, Philip J.},
	keywords = {deep inference},
	pages = {299--345},
	publisher = {Springer},
	series = {Outstanding Contributions to Logic},
	title = {Pomset Logic},
	volume = {20},
	year = {2021},
	bdsk-url-1 = {https://doi.org/10.1007/978-3-030-66545-6%5C_9}}

@inproceedings{Reto:20:Flag:-A-:ig,
	author = {Retoré, Christian},
	booktitle = {Linearity \& Trends in Linear Logic and Applications (Linearity\&TLLA)},
	date-added = {2022-11-02 19:39:44 +0000},
	date-modified = {2022-11-02 19:39:44 +0000},
	doi = {10.4204/eptcs.353.8},
	editor = {Dal Lago, Ugo and de Paiva, Valeria},
	keywords = {deep inference},
	pages = {157--174},
	publisher = {Open Publishing Association},
	series = {Electronic Proceedings in Theoretical Computer Science},
	title = {Flag: {A} Self-Dual Modality for Non-Commutative Contraction and Duplication in the Category of Coherence Spaces},
	url = {https://arxiv.org/pdf/2112.14961.pdf},
	volume = {353},
	year = {2020},
	bdsk-url-1 = {https://doi.org/10.4204/eptcs.353.8}}

@misc{Rove::Linear-L:fk,
	author = {Roversi, Luca},
	date-added = {2010-11-28 16:09:08 +0000},
	date-modified = {2016-06-13 06:02:44 +0000},
	keywords = {deep inference},
	title = {Linear Lambda Calculus with Explicit Substitutions as Proof-Search in Deep Inference},
	url = {http://arxiv.org/pdf/1011.3668.pdf},
	bdsk-url-1 = {http://arxiv.org/pdf/1011.3668}}

@techreport{Rove:18:Subatomi:zp,
	author = {Roversi, Luca},
	date-added = {2021-01-25 15:19:21 +0000},
	date-modified = {2021-01-25 15:22:24 +0000},
	institution = {Università di Torino},
	keywords = {deep inference},
	title = {Subatomic Systems Need Not Be Subatomic},
	url = {https://arxiv.org/pdf/1804.08105.pdf},
	year = {2018},
	bdsk-url-1 = {https://arxiv.org/pdf/1804.08105.pdf}}

@article{Rove:12:Extendin:uq,
	author = {Roversi, Luca},
	date-added = {2013-03-07 14:14:31 +0000},
	date-modified = {2016-04-13 09:08:46 +0000},
	doi = {10.1093/logcom/exu033},
	journal = {Journal of Logic and Computation},
	keywords = {deep inference},
	number = {2},
	pages = {677--698},
	title = {A Deep Inference System with a Self-Dual Binder Which Is Complete for Linear Lambda Calculus},
	url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2014-JLC/Roversi2014JLC.pdf},
	volume = {26},
	year = {2016},
	bdsk-url-1 = {http://arxiv.org/pdf/1212.4483v1.pdf},
	bdsk-url-2 = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2014-JLC/Roversi2014JLC.pdf}}

@misc{Rove:12:Communic:kx,
	author = {Roversi, Luca},
	date-added = {2013-03-07 14:28:39 +0000},
	date-modified = {2014-05-08 14:40:14 +0000},
	keywords = {deep inference},
	title = {Communication, and Concurrency with Logic-Based Restriction Inside a Calculus of Structures},
	url = {http://arxiv.org/pdf/1212.4669v1.pdf},
	year = {2012},
	bdsk-url-1 = {http://arxiv.org/pdf/1212.4669v1.pdf}}

@inproceedings{Rove:11:Linear-L:kx,
	author = {Roversi, Luca},
	booktitle = {Typed Lambda Calculi and Applications (TLCA)},
	date-added = {2011-05-04 18:35:05 +0100},
	date-modified = {2016-12-31 18:46:45 +0000},
	doi = {10.1007/978-3-642-21691-6\_16},
	editor = {Ong, Luke},
	keywords = {deep inference},
	pages = {184--197},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Linear Lambda Calculus and Deep Inference},
	url = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2011-TLCA/Roversi2011TLCA.pdf},
	volume = {6690},
	year = {2011},
	bdsk-url-1 = {http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2011-TLCA/Roversi2011TLCA.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-21691-6%5C_16}}

@article{Sham:15:Nested-S:sj,
	author = {Shamkanov, Daniyar},
	date-added = {2016-04-13 11:34:11 +0000},
	date-modified = {2016-04-13 11:44:10 +0000},
	doi = {10.1093/jigpal/jzv029},
	journal = {Logic Journal of the {IGPL}},
	keywords = {deep inference},
	number = {5},
	pages = {789--815},
	title = {Nested Sequents for Provability Logic {GLP}},
	url = {http://arxiv.org/pdf/1410.6652.pdf},
	volume = {23},
	year = {2015},
	bdsk-url-1 = {http://arxiv.org/pdf/1410.6652.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1093/jigpal/jzv029}}

@inproceedings{SherHeijGundPari:20:Spinal-A:xu,
	author = {Sherratt, David and Heijltjes, Willem and Gundersen, Tom and Parigot, Michel},
	booktitle = {Foundations of Software Science and Computation Structures (FoSSaCS)},
	date-added = {2020-12-09 19:48:22 +0000},
	date-modified = {2020-12-09 19:55:59 +0000},
	doi = {10.1007/978-3-030-45231-5\_30},
	editor = {Goubault-Larrecq, Jean and König, Barbara},
	keywords = {deep inference},
	pages = {582--601},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Spinal Atomic Lambda-Calculus},
	url = {http://www.cs.bath.ac.uk/~wbh22/pdf/2020-sherratt-heijltjes-gundersen-parigot.pdf},
	volume = {12077},
	year = {2020},
	bdsk-url-1 = {http://www.cs.bath.ac.uk/~wbh22/pdf/2020-sherratt-heijltjes-gundersen-parigot.pdf},
	bdsk-url-2 = {https://doi.org/10.1007/978-3-030-45231-5%5C_30}}

@phdthesis{Sher:19:A-Lambda:ve,
	author = {Sherratt, David Rhys},
	date-added = {2022-11-03 13:00:35 +0000},
	date-modified = {2022-11-03 13:02:06 +0000},
	keywords = {deep inference},
	school = {University of Bath},
	title = {A Lambda-Calculus That Achieves Full Laziness with Spine Duplication},
	url = {https://purehost.bath.ac.uk/ws/portalfiles/portal/195822310/thesis_template.pdf},
	year = {2019},
	bdsk-url-1 = {https://purehost.bath.ac.uk/ws/portalfiles/portal/195822310/thesis_template.pdf}}

@inproceedings{SimmKiss:22:Higher-O:rs,
	author = {Simmons, Will and Kissinger, Aleks},
	booktitle = {47th International Symposium on Mathematical Foundations of Computer Science (MFCS)},
	date-added = {2022-11-02 19:39:44 +0000},
	date-modified = {2022-11-02 19:39:44 +0000},
	doi = {10.4230/LIPIcs.MFCS.2022.80},
	editor = {Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
	keywords = {deep inference},
	pages = {80:1--14},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {Higher-Order Causal Theories Are Models of BV-Logic},
	url = {https://drops.dagstuhl.de/opus/volltexte/2022/16878/pdf/LIPIcs-MFCS-2022-80.pdf},
	volume = {241},
	year = {2022},
	bdsk-url-1 = {https://drops.dagstuhl.de/opus/volltexte/2022/16878/pdf/LIPIcs-MFCS-2022-80.pdf},
	bdsk-url-2 = {https://doi.org/10.4230/LIPIcs.MFCS.2022.80}}

@inproceedings{StewStou:05:A-System:tg,
	author = {Stewart, Charles and Stouppa, Phiniki},
	booktitle = {Advances in Modal Logic (AiML)},
	date-modified = {2014-04-26 17:06:13 +0000},
	editor = {Renate Schmidt and Ian Pratt-Hartmann and Mark Reynolds and Heinrich Wansing},
	keywords = {deep inference},
	pages = {309--333},
	publisher = {King's College Publications},
	title = {A Systematic Proof Theory for Several Modal Logics},
	url = {http://www.aiml.net/volumes/volume5/Stewart.ps},
	volume = {5},
	year = {2005},
	bdsk-url-1 = {http://www.aiml.net/volumes/volume5/Stewart.ps}}

@article{Stou:06:A-Deep-I:rt,
	author = {Stouppa, Phiniki},
	date-modified = {2016-12-31 18:19:57 +0000},
	doi = {10.1007/s11225-007-9028-y},
	journal = {Studia Logica},
	keywords = {deep inference},
	number = {2},
	pages = {199--214},
	title = {A Deep Inference System for the Modal Logic {S5}},
	url = {http://www.iam.unibe.ch/tilpub/2007/sto07.pdf},
	volume = {85},
	year = {2007},
	bdsk-url-1 = {http://www.iam.unibe.ch/tilpub/2007/sto07.pdf}}

@mastersthesis{Stou:04:The-Desi:vg,
	author = {Stouppa, Phiniki},
	date-modified = {2008-01-28 14:42:34 +0000},
	keywords = {deep inference},
	school = {Technische Universität Dresden},
	title = {The Design of Modal Proof Theories: The case of {S5}},
	url = {http://www.wv.inf.tu-dresden.de/Publications/Diploma/diplom_stouppa.pdf},
	year = {2004},
	bdsk-url-1 = {http://www.wv.inf.tu-dresden.de/Publications/Diploma/diplom_stouppa.pdf}}

@article{Stra:18:Deep-Inf:zf,
	author = {Straßburger, Lutz},
	date-added = {2019-04-04 22:04:03 +0100},
	date-modified = {2019-11-10 18:05:15 +0000},
	doi = {10.1017/S0960129518000385},
	journal = {Mathematical Structures in Computer Science},
	keywords = {deep inference},
	number = {8},
	pages = {1030--1060},
	title = {Deep Inference and Expansion Trees for Second-Order Multiplicative Linear Logic},
	url = {https://hal.inria.fr/hal-01942410/document},
	volume = {29},
	year = {2019},
	bdsk-url-1 = {https://hal.inria.fr/hal-01942410/document},
	bdsk-url-2 = {https://doi.org/10.1017/S0960129518000385}}

@inproceedings{Stra:17:Combinat:qf,
	author = {Straßburger, Lutz},
	booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD)},
	date-added = {2017-09-17 17:09:01 +0000},
	date-modified = {2017-09-17 17:13:02 +0000},
	doi = {10.4230/LIPIcs.FSCD.2017.31},
	editor = {Miller, Dale},
	keywords = {deep inference},
	pages = {31:1--17},
	publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
	series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	title = {Combinatorial Flows and Their Normalisation},
	url = {http://drops.dagstuhl.de/opus/volltexte/2017/7720/pdf/LIPIcs-FSCD-2017-31.pdf},
	volume = {84},
	year = {2017},
	bdsk-url-1 = {http://drops.dagstuhl.de/opus/volltexte/2017/7720/pdf/LIPIcs-FSCD-2017-31.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2017.31}}

@techreport{Stra:17:Combinat:zl,
	author = {Straßburger, Lutz},
	date-added = {2017-04-02 08:27:04 +0000},
	date-modified = {2017-04-02 08:41:38 +0000},
	institution = {INRIA},
	keywords = {deep inference},
	number = {RR-9048},
	title = {Combinatorial Flows and Proof Compression},
	url = {https://hal.inria.fr/hal-01498468/document},
	year = {2017},
	bdsk-url-1 = {https://hal.inria.fr/hal-01498468/document}}

@inproceedings{Stra:12:Nested-S:uq,
	author = {Straßburger, Lutz},
	booktitle = {Foundations of Software Science and Computation Structures (FoSSaCS)},
	date-added = {2012-07-07 13:24:04 +0100},
	date-modified = {2014-04-26 14:58:04 +0000},
	doi = {10.1007/978-3-642-37075-5\_14},
	editor = {Pfenning, Frank},
	keywords = {deep inference},
	pages = {209--224},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Cut Elimination in Nested Sequents for Intuitionistic Modal Logics},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/nested-int-mod-fossacs13.pdf},
	volume = {7794},
	year = {2013},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/nested-int-mod-fossacs13.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1007/978-3-642-37075-5%5C_14}}

@article{Stra:08:Extensio:kk,
	author = {Straßburger, Lutz},
	date-added = {2008-07-01 11:58:02 +0100},
	date-modified = {2014-04-12 10:44:11 +0000},
	doi = {10.1016/j.apal.2012.07.004},
	journal = {Annals of Pure and Applied Logic},
	keywords = {deep inference},
	number = {12},
	pages = {1995--2007},
	title = {Extension Without Cut},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/psppp.pdf},
	volume = {163},
	year = {2012},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/psppp.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1016/j.apal.2012.07.004}}

@article{StraGugl:09:A-System:vn,
	author = {Straßburger, Lutz and Guglielmi, Alessio},
	date-added = {2009-03-30 09:16:04 +0200},
	date-modified = {2016-06-13 06:04:32 +0000},
	doi = {10.1145/1970398.1970399},
	journal = {ACM Transactions on Computational Logic},
	keywords = {deep inference},
	number = {4},
	pages = {23:1--39},
	title = {A System of Interaction and Structure {IV}: {T}he Exponentials and Decomposition},
	url = {http://arxiv.org/pdf/0903.5259.pdf},
	volume = {12},
	year = {2011},
	bdsk-url-1 = {http://arxiv.org/pdf/0903.5259},
	bdsk-url-2 = {http://dx.doi.org/10.1145/1970398.1970399}}

@article{Stra:09:From-Dee:fr,
	author = {Straßburger, Lutz},
	date-added = {2009-09-03 08:25:28 +0200},
	date-modified = {2016-12-31 18:11:11 +0000},
	doi = {10.1093/logcom/exp047},
	journal = {Journal of Logic and Computation},
	keywords = {deep inference},
	number = {4},
	pages = {589--624},
	title = {From Deep Inference to Proof Nets Via Cut Elimination},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/deepnet.pdf},
	volume = {21},
	year = {2011},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/deepnet.pdf}}

@unpublished{Stra:11:Towards-:fk,
	author = {Straßburger, Lutz},
	date-added = {2011-01-17 14:26:13 +0000},
	date-modified = {2011-01-17 14:27:45 +0000},
	keywords = {deep inference},
	note = {Habilitation Thesis},
	school = {Université Paris VII - Denis Diderot},
	title = {Towards a Theory of Proofs of Classical Logic},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/HDR.pdf},
	year = {2011},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/HDR.pdf}}

@inproceedings{Stra:10:What-Is-:fk,
	author = {Straßburger, Lutz},
	booktitle = {Programs, Proofs, Processes---6th Conference on Computability in Europe},
	date-added = {2010-07-17 18:29:43 +0200},
	date-modified = {2016-12-31 10:08:21 +0000},
	doi = {10.1007/978-3-642-13962-8\_45},
	editor = {Ferreira, Fernando and Löwe, Benedikt and Mayordomo, Elvira and Mendes Gomes, Luís},
	keywords = {deep inference},
	pages = {406--416},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {What Is the Problem with Proof Nets for Classical Logic?},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/CiE10.pdf},
	volume = {6158},
	year = {2010},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/CiE10.pdf}}

@inproceedings{Strasburger:2008qf,
	author = {Straßburger, Lutz},
	booktitle = {Typed Lambda Calculi and Applications (TLCA)},
	date-added = {2008-05-19 11:32:46 +0100},
	date-modified = {2016-12-31 10:07:59 +0000},
	doi = {10.1007/978-3-642-02273-9\_23},
	editor = {Curien, Pierre-Louis},
	keywords = {deep inference},
	pages = {309--324},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/ObsPT-MLL2-finalforTLCA09.pdf},
	volume = {5608},
	year = {2009},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/ObsPT-MLL2-finalforTLCA09.pdf}}

@inproceedings{Stra:07:A-Charac:fk,
	author = {Straßburger, Lutz},
	booktitle = {18th International Conference on Rewriting Techniques and Applications (RTA)},
	date-modified = {2016-12-31 10:06:46 +0000},
	doi = {10.1007/978-3-540-73449-9\_26},
	editor = {Baader, Franz},
	keywords = {deep inference},
	pages = {344--358},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {A Characterisation of Medial as Rewriting Rule},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/CharMedial.pdf},
	volume = {4533},
	year = {2007},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/CharMedial.pdf}}

@inproceedings{Stra:07:Deep-Inf:uq,
	author = {Straßburger, Lutz},
	booktitle = {International Workshop on Hybrid Logic HyLo 2007},
	date-added = {2007-08-26 12:31:10 +0100},
	date-modified = {2007-08-26 12:39:44 +0100},
	editor = {Jørgen Villadsen and Thomas Bolander and Torben Braüner},
	keywords = {deep inference},
	pages = {13--22},
	title = {Deep Inference for Hybrid Logic},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/hybrid.pdf},
	year = {2007},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/hybrid.pdf}}

@article{Stra:06:On-the-A:jy,
	author = {Straßburger, Lutz},
	date-modified = {2012-03-25 22:00:21 +0100},
	journal = {Theory and Applications of Categories},
	keywords = {deep inference},
	number = {18},
	pages = {536--601},
	title = {On the Axiomatisation of Boolean Categories with and Without Medial},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/medial.pdf},
	volume = {18},
	year = {2007},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/medial.pdf}}

@incollection{Stra:05:What-Is-:wl,
	author = {Straßburger, Lutz},
	booktitle = {Logica Universalis---Towards a General Theory of Logic},
	date-modified = {2008-01-15 06:56:32 +0000},
	editor = {Jean-Yves Beziau},
	keywords = {deep inference},
	pages = {135--152},
	publisher = {Birkhäuser},
	title = {What Is a Logic, and What Is a Proof?},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/WhatLogicProof.pdf},
	year = {2007},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/WhatLogicProof.pdf}}

@techreport{Stra:06:Proof-Ne:fk,
	author = {Straßburger, Lutz},
	date-added = {2007-10-10 11:01:54 +0100},
	date-modified = {2016-06-13 06:18:49 +0000},
	institution = {INRIA},
	keywords = {deep inference},
	number = {6013},
	title = {Proof Nets and the Identity of Proofs},
	url = {https://hal.inria.fr/file/index/docid/114320/filename/RR-6013.pdf},
	year = {2006},
	bdsk-url-1 = {http://hal.inria.fr/docs/00/11/43/20/PDF/RR-6013.pdf}}

@unpublished{Stra:06:What-Cou:vh,
	author = {Straßburger, Lutz},
	date-added = {2006-07-03 07:43:21 +0100},
	date-modified = {2013-07-07 23:01:22 +0000},
	keywords = {deep inference},
	note = {Workshop Classical Logic and Computation colocated with ICALP 2006},
	title = {What Could a Boolean Category Be?},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/medial-kurz.pdf},
	year = {2006},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/medial-kurz.pdf}}

@inproceedings{Stra:05:From-Dee:yb,
	author = {Straßburger, Lutz},
	booktitle = {Structures and Deduction},
	date-modified = {2009-09-03 09:01:47 +0200},
	editor = {Paola Bruscoli and François Lamarche and Charles Stewart},
	keywords = {deep inference},
	note = {ICALP Workshop. ISSN 1430-211X},
	pages = {2--18},
	publisher = {Technische Universität Dresden},
	title = {From Deep Inference to Proof Nets},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/deepnet-SD05.pdf},
	year = {2005},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/deepnet-SD05.pdf}}

@inproceedings{StraLama:04:On-Proof:ec,
	author = {Straßburger, Lutz and Lamarche, François},
	booktitle = {Computer Science Logic (CSL)},
	date-modified = {2016-12-31 10:07:12 +0000},
	doi = {10.1007/978-3-540-30124-0\_14},
	editor = {J. Marcinkowski and A. Tarlecki},
	keywords = {deep inference},
	pages = {145--159},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {On Proof Nets for Multiplicative Linear Logic with Units},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/multPN.pdf},
	volume = {3210},
	year = {2004},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/multPN.pdf}}

@phdthesis{Stra:03:Linear-L:lp,
	author = {Straßburger, Lutz},
	date-modified = {2006-07-13 13:12:57 +0100},
	keywords = {deep inference},
	school = {Technische Universität Dresden},
	title = {Linear Logic and Noncommutativity in the Calculus of Structures},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/dissvonlutz.pdf},
	year = {2003},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/dissvonlutz.pdf}}

@article{Stra:03:MELL-in-:oy,
	author = {Straßburger, Lutz},
	date-modified = {2016-12-31 18:20:39 +0000},
	doi = {10.1016/S0304-3975(03)00240-8},
	journal = {Theoretical Computer Science},
	keywords = {deep inference},
	pages = {213--285},
	title = {{MELL} in the Calculus of Structures},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/els.pdf},
	volume = {309},
	year = {2003},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/els.pdf}}

@inproceedings{Stra:03:System-N:mb,
	author = {Straßburger, Lutz},
	booktitle = {10th Workshop on Logic, Language, Information and Computation (WoLLIC)},
	date-added = {2007-03-29 10:00:53 +0100},
	date-modified = {2016-12-31 09:53:24 +0000},
	doi = {10.1016/S1571-0661(04)80853-3},
	editor = {de Queiroz, Ruy and Pimentel, Elaine and Figueiredo, Lucília},
	keywords = {deep inference},
	pages = {166-177},
	publisher = {Elsevier},
	series = {Electronic Notes in Theoretical Computer Science},
	title = {System {NEL} Is Undecidable},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/NELundec_wollic03.pdf},
	volume = {84},
	year = {2003},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/NELundec_wollic03.pdf},
	bdsk-url-2 = {http://dx.doi.org/10.1016/S1571-0661(04)80853-3}}

@techreport{Stra:03:The-Unde:gn,
	author = {Straßburger, Lutz},
	date-modified = {2006-07-13 13:12:59 +0100},
	institution = {Technische Universität Dresden},
	keywords = {deep inference},
	number = {WV-03-05},
	title = {The Undecidability of System {NEL}},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/NELundeci.pdf},
	year = {2003},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/NELundeci.pdf}}

@techreport{Stra:02:A-Local-:ve,
	author = {Straßburger, Lutz},
	date-modified = {2006-07-13 13:12:54 +0100},
	institution = {Technische Universität Dresden},
	keywords = {deep inference},
	number = {WV-02-01},
	title = {A Local System for Linear Logic},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/lls.pdf},
	year = {2002},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/lls.pdf}}

@inproceedings{Stra:02:A-Local-:ul,
	author = {Straßburger, Lutz},
	booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)},
	date-modified = {2016-12-31 10:07:36 +0000},
	doi = {10.1007/3-540-36078-6\_26},
	editor = {Baaz, Matthias and Voronkov, Andrei},
	keywords = {deep inference},
	pages = {388--402},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {A Local System for Linear Logic},
	url = {http://www.lix.polytechnique.fr/~lutz/papers/lls-lpar.pdf},
	volume = {2514},
	year = {2002},
	bdsk-url-1 = {http://www.lix.polytechnique.fr/~lutz/papers/lls-lpar.pdf}}

@inproceedings{TiuIanoGore:12:Grammar-:uq,
	author = {Tiu, Alwen and Ianovski, Egor and Goré, Rajeev},
	booktitle = {Advances in Modal Logic (AiML)},
	date-added = {2012-07-08 16:35:55 +0100},
	date-modified = {2014-04-26 17:06:13 +0000},
	editor = {Bolander, Thomas and Braüner, Torben and Ghilardi, Silvio and Lawrence Moss},
	keywords = {deep inference},
	pages = {516--537},
	publisher = {College Publications},
	title = {Grammar Logics in Nested Sequent Calculus: {P}roof Theory and Decision Procedures},
	url = {http://users.cecs.anu.edu.au/~tiu/papers/grammar.pdf},
	volume = {9},
	year = {2012},
	bdsk-url-1 = {http://users.cecs.anu.edu.au/~tiu/papers/grammar.pdf}}

@inproceedings{Tiu:06:A-Local-:gf,
	author = {Tiu, Alwen},
	booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)},
	date-modified = {2017-10-24 14:24:41 +0000},
	doi = {10.1007/11916277\_17},
	editor = {Hermann, Miki and Voronkov, Andrei},
	keywords = {deep inference},
	pages = {242--256},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {A Local System for Intuitionistic Logic},
	url = {http://users.cecs.anu.edu.au/~tiu/papers/lpar06sub.pdf},
	volume = {4246},
	year = {2006},
	bdsk-url-1 = {http://users.cecs.anu.edu.au/~tiu/localint.pdf}}

@article{Tiu:06:A-System:ai,
	author = {Tiu, Alwen},
	date-modified = {2016-06-13 06:20:05 +0000},
	doi = {10.2168/LMCS-2(2:4)2006},
	journal = {Logical Methods in Computer Science},
	keywords = {deep inference},
	number = {2},
	pages = {4:1--24},
	title = {A System of Interaction and Structure {II}: {T}he Need for Deep Inference},
	url = {https://arxiv.org/pdf/cs/0512036.pdf},
	volume = {2},
	year = {2006},
	bdsk-url-1 = {http://arxiv.org/pdf/cs.LO/0512036},
	bdsk-url-2 = {http://arxiv.org/pdf/cs.LO/0512036.pdf},
	bdsk-url-3 = {http://dx.doi.org/10.2168/LMCS-2(2:4)2006}}

@techreport{Tiu:01:A1-Unifi:ij,
	author = {Tiu, Alwen Fernanto},
	date-modified = {2017-10-24 13:46:29 +0000},
	institution = {Technische Universität Dresden},
	keywords = {deep inference},
	number = {WV-01-08},
	title = {{A1}-Unification},
	url = {http://www.lix.polytechnique.fr/~tiu/a1.ps.gz},
	year = {2001},
	bdsk-url-1 = {http://users.cecs.anu.edu.au/~tiu/a1.ps.gz}}

@techreport{Tiu:01:Combinin:qf,
	author = {Tiu, Alwen Fernanto},
	date-modified = {2017-10-24 13:46:53 +0000},
	institution = {Technische Universität Dresden},
	keywords = {deep inference},
	number = {WV-01-09},
	title = {Combining {A1}- and {AC1}-Unification Sharing Unit},
	url = {http://www.lix.polytechnique.fr/~tiu/comb4.ps.gz},
	year = {2001},
	bdsk-url-1 = {http://users.cecs.anu.edu.au/~tiu/comb4.ps.gz}}

@techreport{Tiu:01:Properti:zk,
	author = {Tiu, Alwen Fernanto},
	date-modified = {2017-10-24 13:47:21 +0000},
	institution = {Technische Universität Dresden},
	keywords = {deep inference},
	number = {WV-01-06},
	title = {Properties of a Logical System in the Calculus of Structures},
	url = {http://www.lix.polytechnique.fr/~tiu/thesisc.pdf},
	year = {2001},
	bdsk-url-1 = {http://users.cecs.anu.edu.au/~tiu/thesisc.pdf}}