%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/


%% Created for Alessio Guglielmi at 2013-04-23 20:03:10 +0100 


%% Saved with string encoding Unicode (UTF-8) 



@inproceedings{alenda2012nested,
	Author = {Alenda, R{\'e}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 = {2013-03-05 21:16:23 +0000},
	Editor = {Fari{\~n}as del Cerro, Luis and Herzig, Andreas and Mengin, J{\'e}r{\^o}me},
	Keywords = {deep inference},
	Note = {\url{http://www.di.unito.it/~argo/papers/2012_JELIAb.pdf}},
	Pages = {14--27},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {Nested Sequent Calculi for Conditional Logics},
	Volume = {7519},
	Year = {2012}}

@inproceedings{Bilk:11:A-Note-o:fk,
	Author = {B{\'\i}lkov{\'a}, Marta},
	Booktitle = {Logic, Language, and Computation (TbiLLC 2009)},
	Date-Added = {2013-03-05 19:49:05 +0000},
	Date-Modified = {2013-03-05 19:56:05 +0000},
	Editor = {Bezhanishvili, Nick and L{\"o}bner, Sebastian and Schwabe, Kerstin and Spada, Luca},
	Keywords = {deep inference},
	Pages = {30--45},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Artificial Intelligence},
	Title = {A Note on Uniform Interpolation Proofs in Modal Deep Inference Calculi},
	Volume = {6618},
	Year = {2011}}

@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 = {2012-07-05 18:00:30 +0100},
	Journal = {Applied Categorical Structures},
	Keywords = {deep inference},
	Note = {\url{http://www.cs.mcgill.ca/~prakash/Pubs/seqcats.pdf}},
	Pages = {209--228},
	Title = {Deep Inference and Probabilistic Coherence Spaces},
	Volume = {20},
	Year = {2012}}

@unpublished{BlutGuglIvanPana:10:A-Logica:uq,
	Author = {Blute, Richard F. and Guglielmi, Alessio and Ivanov, Ivan T. and Panangaden, Prakash and Stra{\ss}burger, Lutz},
	Date-Added = {2010-06-01 10:20:30 +0200},
	Date-Modified = {2011-06-13 15:07:44 +0100},
	Keywords = {deep inference},
	Note = {Submitted. \url{http://cs.bath.ac.uk/ag/p/LBQEE.pdf}},
	Title = {A Logical Basis for Quantum Evolution and Entanglement},
	Year = {2011}}

@inproceedings{BlutPanaStra:08:The-Logi:lh,
	Author = {Blute, Rick and Panangaden, Prakash and Stra{\ss}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 = {2010-06-01 10:41:44 +0200},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/BVlocative.pdf}},
	Title = {The Logic {BV} and Quantum Causality},
	Year = {2008}}

@incollection{BrunGugl:04:A-First-:ys,
	Author = {Br{\"u}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},
	Note = {\url{http://www.iam.unibe.ch/~kai/Papers/FinFOL.pdf}},
	Pages = {59--74},
	Publisher = {Logos Verlag},
	Series = {Logische Philosophie},
	Title = {A First Order System with Finite Choice of Premises},
	Year = 2004}

@inproceedings{BrunTiu:01:A-Local-:mz,
	Author = {Br{\"u}nnler, Kai and Tiu, Alwen Fernanto},
	Booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)},
	Date-Modified = {2011-12-29 09:37:19 +0000},
	Editor = {R. Nieuwenhuis and Voronkov, Andrei},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/~kai/Papers/lcl-lpar.pdf}},
	Pages = {347--361},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {A Local System for Classical Logic},
	Volume = 2250,
	Year = 2001}

@techreport{BrunTiu:01:A-Local-:ly,
	Author = {Br{\"u}nnler, Kai and Tiu, Alwen Fernanto},
	Date-Modified = {2006-07-13 13:12:54 +0100},
	Institution = {Technische Universit{\"a}t Dresden},
	Keywords = {deep inference},
	Note = {\url{http://iccl.tu-dresden.de/~kai/LocalClassicalLogic-tr.pdf}},
	Number = {WV-01-02},
	Title = {A Local System for Classical Logic},
	Year = 2001}

@inproceedings{BrunGoetKuzn:10:A-Syntac:uq,
	Author = {Br{\"u}nnler, Kai and Goetschi, Remo and Kuznets, Roman},
	Booktitle = {Advances in Modal Logic},
	Date-Added = {2010-11-28 17:17:19 +0000},
	Date-Modified = {2010-11-28 17:24:57 +0000},
	Editor = {Lev Beklemishev and Valentin Goranko and Valentin Shehtman},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/~kai/Papers/2010srtjl.pdf}},
	Pages = {39--58},
	Publisher = {College Publications},
	Title = {A Syntactic Realization Theorem for Justification Logics},
	Volume = {8},
	Year = {2010}}

@inproceedings{BrunMcKi:08:An-Algor:wq,
	Author = {Br{\"u}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 = {2011-12-29 09:37:15 +0000},
	Editor = {Cervesato, Iliano and Veith, Helmut and Voronkov, Andrei},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/~kai/Papers/2008aidis.pdf}},
	Pages = {482---496},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {An Algorithmic Interpretation of a Deep Inference System},
	Volume = {5330},
	Year = {2008}}

@inproceedings{Brun:03:Atomic-C:oz,
	Author = {Br{\"u}nnler, Kai},
	Booktitle = {Computer Science Logic (CSL)},
	Date-Modified = {2011-12-29 09:32:14 +0000},
	Editor = {M. Baaz and J. A. Makowsky},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/~kai/Papers/ace.pdf}},
	Pages = {86--97},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {Atomic Cut Elimination for Classical Logic},
	Volume = 2803,
	Year = 2003}

@techreport{BrunGugl:02:Consiste:kn,
	Author = {Br{\"u}nnler, Kai and Guglielmi, Alessio},
	Date-Modified = {2006-07-13 13:12:55 +0100},
	Institution = {Technische Universit{\"a}t Dresden},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/AG4.pdf}},
	Number = {WV-02-16},
	Title = {Consistency Without Cut Elimination},
	Year = 2002}

@article{Brun:06:Cut-Elim:cq,
	Author = {Br{\"u}nnler, Kai},
	Date-Modified = {2006-07-13 13:12:55 +0100},
	Journal = {Studia Logica},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/~kai/Papers/q.pdf}},
	Number = {1},
	Pages = {51--71},
	Title = {Cut Elimination Inside a Deep Inference System for Classical Predicate Logic},
	Volume = {82},
	Year = 2006}

@inproceedings{Brun:06:Deep-Inf:qy,
	Author = {Br{\"u}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 = {2010-07-17 19:46:08 +0200},
	Editor = {Beckmann, Arnold and Berger, Ulrich and L{\"o}we, Benedikt and Tucker, John V.},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/~kai/Papers/n.pdf}},
	Pages = {65--74},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {Deep Inference and Its Normal Form of Derivations},
	Volume = {3988},
	Year = {2006}}

@book{Brun:04:Deep-Inf:rq,
	Address = {Berlin},
	Author = {Br{\"u}nnler, Kai},
	Date-Modified = {2006-07-13 13:12:55 +0100},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/~kai/Papers/phd.pdf}},
	Publisher = {Logos Verlag},
	Title = {Deep Inference and Symmetry in Classical Proofs},
	Year = 2004}

@article{Brun:07:Deep-Seq:fk,
	Author = {Br{\"u}nnler, Kai},
	Date-Added = {2007-08-26 10:54:46 +0100},
	Date-Modified = {2010-04-13 19:17:37 +0200},
	Journal = {Archive for Mathematical Logic},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/~kai/Papers/2009dssml.pdf}},
	Number = {6},
	Pages = {551--577},
	Title = {Deep Sequent Systems for Modal Logic},
	Volume = {48},
	Year = {2009}}

@inproceedings{Brun::Deep-Seq:ay,
	Author = {Br{\"u}nnler, Kai},
	Booktitle = {Advances in Modal Logic},
	Date-Added = {2006-03-30 17:44:13 +0100},
	Date-Modified = {2006-09-07 11:10:13 +0100},
	Editor = {Guido Governatori and Ian Hodkinson and Yde Venema},
	Keywords = {deep inference},
	Note = {\url{http://www.aiml.net/volumes/volume6/Bruennler.ps}},
	Pages = {107--119},
	Publisher = {College Publications},
	Title = {Deep Sequent Systems for Modal Logic},
	Volume = {6},
	Year = {2006}}

@inproceedings{Brun:10:How-to-U:kx,
	Author = {Br{\"u}nnler, Kai},
	Booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17)},
	Date-Added = {2010-11-28 17:53:20 +0000},
	Date-Modified = {2011-12-29 09:37:11 +0000},
	Editor = {Ferm{\"u}ller, Christian G. and Voronkov, Andrei},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/~kai/Papers/2010hucer.pdf}},
	Pages = {172--186},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {How to Universally Close the Existential Rule},
	Volume = {6397},
	Year = {2010}}

@article{Brun:06:Locality:zh,
	Author = {Br{\"u}nnler, Kai},
	Date-Modified = {2007-05-29 09:47:02 +0100},
	Journal = {Notre Dame Journal of Formal Logic},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/~kai/Papers/LocalityClassical.pdf}},
	Number = {4},
	Pages = {557--580},
	Title = {Locality for Classical Logic},
	Volume = {47},
	Year = 2006}

@inproceedings{BrunStra:09:Modular-:ys,
	Author = {Br{\"u}nnler, Kai and Stra{\ss}burger, Lutz},
	Booktitle = {Tableaux 2009},
	Date-Added = {2009-05-08 16:15:49 +0200},
	Date-Modified = {2010-04-13 19:31:52 +0200},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/~kai/Papers/2009mssml.pdf}},
	Pages = {152--166},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Artificial Intelligence},
	Title = {Modular Sequent Systems for Modal Logic},
	Volume = {5607},
	Year = {2009}}

@unpublished{Brun:10:Nested-S:fk,
	Author = {Br{\"u}nnler, Kai},
	Date-Added = {2010-04-13 18:27:25 +0200},
	Date-Modified = {2011-01-25 16:40:12 +0000},
	Keywords = {deep inference},
	Note = {Habilitation Thesis. \url{http://arxiv.org/pdf/1004.1845}},
	School = {Universit{\"a}t Bern},
	Title = {Nested Sequents},
	Year = {2010}}

@inproceedings{BrunLeng:05:On-Two-F:jf,
	Author = {Br{\"u}nnler, Kai and Lengrand, St{\'e}phane},
	Booktitle = {Structures and Deduction},
	Date-Modified = {2006-12-24 12:12:26 +0000},
	Editor = {Paola Bruscoli and Fran{\c c}ois Lamarche and Charles Stewart},
	Keywords = {deep inference},
	Note = {ICALP Workshop. ISSN 1430-211X. \url{http://www.iam.unibe.ch/~kai/Papers/sd05.pdf}},
	Pages = {69--80},
	Publisher = {Technische Universit{\"a}t Dresden},
	Title = {On Two Forms of Bureaucracy in Derivations},
	Year = 2005}

@article{BrunStud:12:Syntacti:fk,
	Author = {Br{\"u}nnler, Kai and Studer, Thomas},
	Date-Added = {2013-04-23 17:43:44 +0100},
	Date-Modified = {2013-04-23 17:49:36 +0100},
	Journal = {Annals of Pure and Applied Logic},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/ltgpub/2012/bs12.pdf}},
	Number = {12},
	Pages = {1838---1853},
	Title = {Syntactic Cut-Elimination for a Fragment of the Modal Mu-Calculus},
	Volume = {163},
	Year = {2012}}

@article{BrunStud:09:Syntacti:yq,
	Author = {Br{\"u}nnler, Kai and Studer, Thomas},
	Date-Added = {2009-05-06 13:13:02 +0200},
	Date-Modified = {2013-04-23 17:49:25 +0100},
	Journal = {Annals of Pure and Applied Logic},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/~kai/Papers/infck.pdf}},
	Number = {1},
	Pages = {82--95},
	Title = {Syntactic Cut-Elimination for Common Knowledge},
	Volume = {160},
	Year = {2009}}

@inproceedings{BrunStud::Syntacti:vn,
	Author = {Br{\"u}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{\'e}phane},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/~kai/Papers/m4m5.pdf}},
	Pages = {227--240},
	Publisher = {Elsevier},
	Series = {Electronic Notes in Theoretical Computer Science},
	Title = {Syntactic Cut-Elimination for Common Knowledge},
	Volume = {231},
	Year = {2009}}

@article{Brun:03:Two-Rest:mn,
	Author = {Br{\"u}nnler, Kai},
	Date-Modified = {2006-07-13 13:12:59 +0100},
	Journal = {Logic Journal of the {IGPL}},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/~kai/Papers/RestContr.pdf}},
	Number = 5,
	Pages = {525--529},
	Title = {Two Restrictions on Contraction},
	Volume = 11,
	Year = 2003}

@inproceedings{Brus:02:A-Purely:wd,
	Author = {Bruscoli, Paola},
	Booktitle = {Logic Programming, 18th International Conference (ICLP)},
	Date-Modified = {2011-12-29 09:23:55 +0000},
	Editor = {Peter J. Stuckey},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/pb/bvl/bvl.pdf}},
	Pages = {302--316},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {A Purely Logical Account of Sequentiality in Proof Search},
	Volume = 2401,
	Year = 2002}

@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 = {2010-07-17 19:47:16 +0200},
	Editor = {Bertram Fronh{\"o}fer and Steffen H{\"o}lldobler},
	Keywords = {deep inference},
	Note = {ISSN 1430--211X},
	Number = {TUD--FI03--03},
	Organization = {TU Dresden, 01062 Dresden},
	Series = {Technische Berichte der Fakult{\"a}t Informatik},
	Title = {A Purely Logical Account of Sequentiality in Proof Search -- Extended Abstract},
	Year = 2002}

@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 = {2011-12-29 09:37:02 +0000},
	Editor = {Clarke, Edmund M. and Voronkov, Andrei},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/QPNDI.pdf}},
	Pages = {136--153},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae},
	Volume = {6355},
	Year = {2010}}

@unpublished{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 = {2011-05-04 17:45:23 +0100},
	Keywords = {deep inference},
	Note = {Submitted. \url{http://cs.bath.ac.uk/ag/p/QPNPDI.pdf}},
	Title = {A Quasipolynomial Normalisation Procedure in Deep Inference},
	Year = {2011}}

@unpublished{BrusGugl:07:On-Analy:uq,
	Author = {Bruscoli, Paola and Guglielmi, Alessio},
	Date-Added = {2007-09-22 14:54:48 +0100},
	Date-Modified = {2007-09-22 14:56:01 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/Onan.pdf}},
	Title = {On Analytic Inference Rules in the Calculus of Structures},
	Year = {2007}}

@unpublished{BrusGugl:09:On-Analy:kx,
	Author = {Bruscoli, Paola and Guglielmi, Alessio},
	Date-Added = {2009-11-23 23:46:58 +0100},
	Date-Modified = {2009-11-23 23:48:53 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/ADI.pdf}},
	Title = {On Analyticity in Deep Inference},
	Year = {2009}}

@article{BrusGugl:07:On-the-P:fk,
	Author = {Bruscoli, Paola and Guglielmi, Alessio},
	Date-Added = {2007-08-25 21:18:04 +0100},
	Date-Modified = {2011-10-20 18:19:36 +0100},
	Journal = {ACM Transactions on Computational Logic},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/PrComplDI.pdf}},
	Number = {2},
	Pages = {14:1--34},
	Title = {On the Proof Complexity of Deep Inference},
	Volume = {10},
	Year = {2009}}

@unpublished{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 = {2010-01-25 09:00:25 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/QuasiPolNormDI.pdf}},
	Title = {Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae},
	Year = {2009}}

@inproceedings{ChauGuenStra:11:The-Focu:fk,
	Author = {Chaudhuri, Kaustuv and Guenot, Nicolas and Stra{\ss}burger, Lutz},
	Booktitle = {Computer Science Logic (CSL))},
	Date-Added = {2012-07-07 12:52:40 +0100},
	Date-Modified = {2012-07-07 13:10:30 +0100},
	Editor = {Bezem, Marc},
	Keywords = {deep inference},
	Note = {\url{http://drops.dagstuhl.de/opus/volltexte/2011/3229/pdf/16.pdf}},
	Pages = {159--173},
	Publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
	Series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	Title = {The Focused Calculus of Structures},
	Volume = {12},
	Year = {2011}}

@inproceedings{Das:12:Complexi:kx,
	Author = {Das, Anupam},
	Booktitle = {Computability in Europe},
	Date-Added = {2012-07-07 15:09:55 +0100},
	Date-Modified = {2012-07-07 17:19:28 +0100},
	Editor = {Cooper, S. Barry and Dawar, Anuj and L{\"o}we, Benedikt},
	Keywords = {deep inference},
	Note = {\url{http://www.anupamdas.com/items/RelComp/RelComp.pdf}},
	Pages = {139--150},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {Complexity of Deep Inference via Atomic Flows},
	Volume = {7318},
	Year = {2012}}

@inproceedings{Das:11:On-the-P:fk,
	Author = {Das, Anupam},
	Booktitle = {Tableaux 2011},
	Date-Added = {2011-05-04 11:55:58 +0100},
	Date-Modified = {2012-03-25 20:07:40 +0100},
	Editor = {Br{\"u}nnler, Kai and Metcalfe, George},
	Keywords = {deep inference},
	Note = {\url{http://www.anupamdas.com/items/PrCompII/ProofComplexityBoundedDI.pdf}},
	Pages = {134--148},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Artificial Intelligence},
	Title = {On the Proof Complexity of Cut-Free Bounded Deep Inference},
	Volume = {6793},
	Year = {2011}}

@inproceedings{Das:13:Rewritin:uq,
	Author = {Das, Anupam},
	Booktitle = {24st International Conference on Rewriting Techniques and Applications},
	Date-Added = {2013-03-05 20:52:11 +0000},
	Date-Modified = {2013-04-06 17:59:29 +0100},
	Keywords = {deep inference},
	Note = {In press. \url{http://www.anupamdas.com/items/RewritingWithLinearInferences/RewritingWithLinearInferences.pdf}},
	Publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
	Series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	Title = {Rewriting with Linear Inferences in Propositional Logic},
	Year = {2013}}

@article{Das:13:Some-Res:fk,
	Author = {Das, Anupam},
	Date-Added = {2013-04-06 17:28:37 +0100},
	Date-Modified = {2013-04-06 17:29:31 +0100},
	Journal = {Logical Methods in Computer Science},
	Keywords = {deep inference},
	Note = {In press. \url{http://www.anupamdas.com/items/RelCompFull/RelCompFull.pdf}},
	Title = {Some Results on the Relative Proof Complexity of Deep Inference Via Atomic Flows},
	Year = {2013}}

@unpublished{Das:13:The-Pige:fk,
	Author = {Das, Anupam},
	Date-Added = {2013-03-05 20:50:34 +0000},
	Date-Modified = {2013-03-05 20:53:02 +0000},
	Keywords = {deep inference},
	Note = {Submitted. \url{http://www.anupamdas.com/items/WeakMonProofsPHP/WeakMonProofsPHP.pdf}},
	Title = {The Pigeonhole Principle and Related Counting Arguments in Weak Monotone Systems},
	Year = {2013}}

@inproceedings{Di-G:04:Structur:wy,
	Author = {Di Gianantonio, Pietro},
	Booktitle = {Computer Science Logic (CSL)},
	Date-Modified = {2011-12-29 09:32:24 +0000},
	Editor = {J. Marcinkowski and A. Tarlecki},
	Keywords = {deep inference},
	Note = {\url{http://www.dimi.uniud.it/~pietro/papers/Soft-copy-ps/scll.ps.gz}},
	Pages = {130--144},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {Structures for Multiplicative Cyclic Linear Logic: {D}eepness Vs Cyclicity},
	Volume = 3210,
	Year = 2004}

@unpublished{Fitt:11:Nested-S:kx,
	Author = {Fitting, Melvin},
	Date-Added = {2012-07-05 17:08:40 +0100},
	Date-Modified = {2012-07-05 17:09:29 +0100},
	Keywords = {deep inference},
	Note = {Submitted. \url{http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/IntuitionisticNested.pdf}},
	Title = {Nested Sequents for Intuitionistic Logics},
	Year = {2011}}

@article{Fitt:12:Prefixed:fk,
	Author = {Fitting, Melvin},
	Date-Added = {2012-07-05 16:01:17 +0100},
	Date-Modified = {2013-04-23 17:48:35 +0100},
	Journal = {Annals of Pure and Applied Logic},
	Keywords = {deep inference},
	Note = {\url{http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/NestedSequentsPostingVersion/PrefixedDeep.pdf}},
	Number = {3},
	Pages = {291--313},
	Title = {Prefixed Tableaus and Nested Sequents},
	Volume = {163},
	Year = {2012}}

@incollection{Fitt:11:Proving-:uq,
	Author = {Fitting, Melvin},
	Booktitle = {Logic without Frontiers},
	Date-Added = {2012-07-05 16:48:58 +0100},
	Date-Modified = {2012-07-05 16:54:46 +0100},
	Editor = {B{\'e}ziau, Jean-Yves and Coniglio, Marcelo Esteban},
	Keywords = {deep inference},
	Note = {\url{http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/Carnielli.pdf}},
	Pages = {145--154},
	Publisher = {College Publications},
	Series = {Tributes},
	Title = {Proving Completeness for Nested Sequent Calculi},
	Year = {2011}}

@article{GoreTiu:06:Classica:uq,
	Author = {Gor{\'e}, Rajeev and Tiu, Alwen},
	Date-Added = {2006-09-13 07:31:25 +0100},
	Date-Modified = {2012-07-08 16:27:55 +0100},
	Journal = {Journal of Logic and Computation},
	Keywords = {deep inference},
	Note = {\url{http://users.cecs.anu.edu.au/~tiu/papers/cmdl.pdf}},
	Number = {4},
	Pages = {767--794},
	Title = {Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-free Deep Inference Calculi for {S5}},
	Volume = {17},
	Year = {2007}}

@inproceedings{GorePostTiu:10:Cut-Elim:vn,
	Author = {Gor{\'e}, Rajeev and Postniece, Linda and Tiu, Alwen},
	Booktitle = {Advances in Modal Logic},
	Date-Added = {2010-11-28 18:18:12 +0000},
	Date-Modified = {2012-07-08 16:28:17 +0100},
	Editor = {Lev Beklemishev and Valentin Goranko and Valentin Shehtman},
	Keywords = {deep inference},
	Note = {\url{http://www.aiml.net/volumes/volume8/Gore-Postniece-Tiu.pdf}},
	Pages = {156--177},
	Publisher = {College Publications},
	Title = {Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic},
	Volume = {8},
	Year = {2010}}

@inproceedings{GorePostTiu:08:Cut-Elim:yq,
	Author = {Gor{\'e}, Rajeev and Postniece, Linda and Tiu, Alwen},
	Booktitle = {Advances in Modal Logic},
	Date-Added = {2009-05-08 15:19:06 +0200},
	Date-Modified = {2012-07-08 16:28:42 +0100},
	Editor = {Carlos Areces and Robert Goldblatt},
	Keywords = {deep inference},
	Note = {\url{http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf}},
	Pages = {43--66},
	Publisher = {College Publications},
	Title = {Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents},
	Volume = {7},
	Year = {2008}}

@inproceedings{GoreRama:12:Labelled:fk,
	Author = {Gor{\'e}, Rajeev and Ramanayake, Revantha},
	Booktitle = {Advances in Modal Logic},
	Date-Added = {2012-07-08 16:26:52 +0100},
	Date-Modified = {2013-03-05 21:13:35 +0000},
	Editor = {Bolander, Thomas and Bra{\"u}ner, Torben and Ghilardi, Silvio and Lawrence Moss},
	Keywords = {deep inference},
	Note = {\url{http://rsise.anu.edu.au/~rpg/Publications/AiML2012/gore-ramanayake-aiml12.pdf}},
	Pages = {279--299},
	Publisher = {College Publications},
	Title = {Labelled Tree sequents, Tree Hypersequents and Nested (Deep) Sequents},
	Volume = {9},
	Year = {2012}}

@article{GorePostTiu:11:On-the-C:fk,
	Author = {Gor{\'e}, Rajeev and Postniece, Linda and Tiu, Alwen},
	Date-Added = {2011-05-05 07:11:03 +0100},
	Date-Modified = {2012-07-08 16:29:12 +0100},
	Journal = {Logical Methods in Computer Science},
	Keywords = {deep inference},
	Note = {\url{http://arxiv.org/pdf/1103.5286}},
	Number = {2},
	Pages = {8:1--38},
	Title = {On the Correspondence Between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics},
	Volume = {7},
	Year = {2011}}

@inproceedings{GorePostTiu:09:Taming-D:rt,
	Author = {Gor{\'e}, Rajeev and Postniece, Linda and Tiu, Alwen},
	Booktitle = {Tableaux 2009},
	Date-Added = {2009-05-08 15:46:50 +0200},
	Date-Modified = {2012-07-08 16:29:34 +0100},
	Keywords = {deep inference},
	Note = {\url{http://users.cecs.anu.edu.au/~tiu/papers/kt.pdf}},
	Pages = {189--204},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Artificial Intelligence},
	Title = {Taming Displayed Tense Logics Using Nested Sequents With Deep Inference},
	Volume = {5607},
	Year = {2009}}

@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 = {2011-05-05 09:54:22 +0100},
	Editor = {Manuel Hermenegildo and Torsten Schaub},
	Keywords = {deep inference},
	Note = {\url{http://drops.dagstuhl.de/opus/volltexte/2010/2586/pdf/10003.GuenotNicolas.2586.pdf}},
	Pages = {84--93},
	Publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
	Series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	Title = {Focused Proof Search for Linear Logic in the Calculus of Structures},
	Volume = {7},
	Year = {2010}}

@phdthesis{Guen:13:Nested-D:uq,
	Author = {Guenot, Nicolas},
	Date-Added = {2013-04-23 18:40:26 +0100},
	Date-Modified = {2013-04-23 18:42:07 +0100},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~nguenot/th/thesis.pdf}},
	School = {{\'E}cole Polytechnique},
	Title = {Nested Deduction in Logical Foundations for Computation},
	Year = {2013}}

@inproceedings{GuglStra:02:A-Non-co:lq,
	Author = {Guglielmi, Alessio and Stra{\ss}burger, Lutz},
	Booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)},
	Date-Modified = {2011-12-29 09:36:42 +0000},
	Editor = {Baaz, Matthias and Voronkov, Andrei},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/NEL.pdf}},
	Pages = {231--246},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {A Non-commutative Extension of {MELL}},
	Volume = 2514,
	Year = 2002}

@inproceedings{GuglGundPari::A-Proof-:fk,
	Author = {Guglielmi, Alessio and Gundersen, Tom and Parigot, Michel},
	Booktitle = {21st International Conference on Rewriting Techniques and Applications},
	Date-Added = {2010-03-15 22:31:13 +0100},
	Date-Modified = {2010-07-17 19:00:33 +0200},
	Editor = {Lynch, Christopher},
	Keywords = {deep inference},
	Note = {\url{http://drops.dagstuhl.de/opus/volltexte/2010/2649}},
	Pages = {135--150},
	Publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
	Series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	Title = {A Proof Calculus Which Reduces Syntactic Bureaucracy},
	Volume = {6},
	Year = {2010}}

@article{Gugl:06:A-System:kl,
	Author = {Guglielmi, Alessio},
	Date-Modified = {2011-10-20 18:20:44 +0100},
	Journal = {ACM Transactions on Computational Logic},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/SystIntStr.pdf}},
	Number = {1},
	Pages = {1:1--64},
	Title = {A System of Interaction and Structure},
	Volume = {8},
	Year = 2007}

@article{GuglStra:02:A-Non-co:dq,
	Author = {Guglielmi, Alessio and Stra{\ss}burger, Lutz},
	Date-Modified = {2011-05-01 19:08:06 +0100},
	Journal = {Mathematical Structures in Computer Science},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/NEL-splitting.pdf}},
	Number = {3},
	Pages = {563--584},
	Title = {A System of Interaction and Structure {V}: {T}he Exponentials and Splitting},
	Volume = {21},
	Year = 2011}

@inproceedings{GuglGundStra::Breaking:uq,
	Author = {Guglielmi, Alessio and Gundersen, Tom and Stra{\ss}burger, Lutz},
	Booktitle = {25th Annual IEEE Symposium on Logic in Computer Science (LICS)},
	Date-Added = {2010-01-25 09:14:10 +0100},
	Date-Modified = {2011-12-29 09:18:10 +0000},
	Editor = {Jouannaud, Jean-Pierre},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/AFII.pdf}},
	Pages = {284--293},
	Publisher = {IEEE},
	Title = {Breaking Paths in Atomic Flows for Classical Logic},
	Year = {2010}}

@unpublished{Gugl:05:Butterfl:mb,
	Author = {Guglielmi, Alessio},
	Date-Modified = {2006-07-13 13:21:34 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/AG7.pdf}},
	Title = {Butterflies},
	Year = {2005}}

@misc{Gugl::Deep-Inf:uq,
	Author = {Guglielmi, Alessio},
	Date-Added = {2007-03-03 16:59:08 +0000},
	Date-Modified = {2009-05-04 01:12:57 +0200},
	Howpublished = {Web site at \url{http://alessio.guglielmi.name/res/cos}},
	Keywords = {deep inference},
	Title = {Deep Inference}}

@unpublished{Gugl:06:Deep-Inf:ap,
	Author = {Guglielmi, Alessio},
	Date-Modified = {2006-07-13 13:21:24 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/CalcStrPR.pdf}},
	Title = {Deep Inference and the Calculus of Structures---{P}roject Report},
	Year = {2006}}

@unpublished{Gugl:04:Formalis:am,
	Author = {Guglielmi, Alessio},
	Date-Modified = {2006-07-13 13:21:10 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/AG11.pdf}},
	Title = {Formalism {A}},
	Year = {2004}}

@unpublished{Gugl:04:Formalis:ea,
	Author = {Guglielmi, Alessio},
	Date-Added = {2006-01-16 10:48:21 +0000},
	Date-Modified = {2006-07-13 13:20:59 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/AG13.pdf}},
	Title = {Formalism {B}},
	Year = {2004}}

@unpublished{Gugl:02:Goodness:ti,
	Author = {Guglielmi, Alessio},
	Date-Modified = {2006-07-13 13:20:23 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/AG1.pdf}},
	Title = {Goodness, Perfection and Miracles},
	Year = {2002}}

@unpublished{Gugl:03:Mismatch:pt,
	Author = {Guglielmi, Alessio},
	Date-Modified = {2006-07-13 13:20:05 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/AG9.pdf}},
	Title = {Mismatch},
	Year = {2003}}

@inproceedings{GuglStra:01:Non-comm:rp,
	Author = {Guglielmi, Alessio and Stra{\ss}burger, Lutz},
	Booktitle = {Computer Science Logic (CSL)},
	Date-Modified = {2011-12-29 09:31:59 +0000},
	Editor = {L. Fribourg},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/NoncMELLCoS.pdf}},
	Pages = {54--68},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {Non-commutativity and {MELL} in the Calculus of Structures},
	Volume = 2142,
	Year = 2001}

@article{GuglGund:07:Normalis:lr,
	Author = {Guglielmi, Alessio and Gundersen, Tom},
	Date-Added = {2007-03-03 11:45:55 +0000},
	Date-Modified = {2011-10-20 18:19:09 +0100},
	Journal = {Logical Methods in Computer Science},
	Keywords = {deep inference},
	Note = {\url{http://www.lmcs-online.org/ojs/viewarticle.php?id=341}},
	Number = {1},
	Pages = {9:1--36},
	Title = {Normalisation Control in Deep Inference via Atomic Flows},
	Volume = {4},
	Year = {2008}}

@unpublished{GuglGund:08:Normalis:yu,
	Author = {Guglielmi, Alessio and Gundersen, Tom},
	Date-Added = {2008-02-22 16:16:51 +0000},
	Date-Modified = {2008-02-22 16:17:46 +0000},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/NormContrDIAtFl2.pdf}},
	Title = {Normalisation Control in Deep Inference via Atomic Flows {II}},
	Year = {2008}}

@unpublished{Gugl:03:Normalis:tf,
	Author = {Guglielmi, Alessio},
	Date-Modified = {2006-07-13 13:19:39 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/AG6.pdf}},
	Title = {Normalisation Without Cut Elimination},
	Year = {2003}}

@unpublished{Gugl:02:On-Lafon:iq,
	Author = {Guglielmi, Alessio},
	Date-Modified = {2006-07-13 13:19:26 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/AG5.pdf}},
	Title = {On {L}afont's Counterexample},
	Year = {2002}}

@unpublished{Gugl:07:On-the-P:fk,
	Author = {Guglielmi, Alessio},
	Date-Added = {2007-08-12 09:31:38 +0200},
	Date-Modified = {2007-08-12 09:41:16 +0200},
	Keywords = {deep inference},
	Note = {Prolog program. \url{http://cs.bath.ac.uk/ag/p/PrComplDI.plg}},
	Title = {On the Proof Complexity of Deep Inference---{C}onjecture},
	Year = {2007}}

@unpublished{Gugl:04:Polynomi:zi,
	Author = {Guglielmi, Alessio},
	Date-Modified = {2006-07-13 13:19:10 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/AG12.pdf}},
	Title = {Polynomial Size Deep-Inference Proofs Instead of Exponential Size Shallow-Inference Proofs},
	Year = {2004}}

@unpublished{Gugl:02:Recipe:xv,
	Author = {Guglielmi, Alessio},
	Date-Modified = {2006-07-13 13:18:56 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/AG2.pdf}},
	Title = {Recipe},
	Year = {2002}}

@unpublished{Gugl:03:Resoluti:ce,
	Author = {Guglielmi, Alessio},
	Date-Modified = {2006-07-13 13:18:41 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/AG10.pdf}},
	Title = {Resolution in the Calculus of Structures},
	Year = {2003}}

@unpublished{Gugl:05:Some-New:eh,
	Author = {Guglielmi, Alessio},
	Date-Added = {2006-01-16 10:48:24 +0000},
	Date-Modified = {2006-07-13 13:17:56 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/AG16.pdf}},
	Title = {Some News on Subatomic Logic},
	Year = {2005}}

@unpublished{Gugl:02:Subatomi:oh,
	Author = {Guglielmi, Alessio},
	Date-Modified = {2006-07-13 13:16:56 +0100},
	Keywords = {deep inference},
	Note = {\url{http://cs.bath.ac.uk/ag/p/AG8.pdf}},
	Title = {Subatomic Logic},
	Year = {2002}}

@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{\c c}ois Lamarche and Charles Stewart},
	Keywords = {deep inference},
	Note = {ICALP Workshop. ISSN 1430-211X. \url{http://cs.bath.ac.uk/ag/p/AG14.pdf}},
	Pages = {53--68},
	Publisher = {Technische Universit{\"a}t Dresden},
	Title = {The Problem of Bureaucracy and Identity of Proofs from the Perspective of Deep Inference},
	Year = 2005}

@misc{Gugl:09:th.pl:rz,
	Author = {Guglielmi, Alessio},
	Date-Added = {2009-02-25 06:54:03 +0100},
	Date-Modified = {2009-02-25 06:58:44 +0100},
	Keywords = {deep inference},
	Note = {Prolog program. \url{http://cs.bath.ac.uk/ag/p/th.pl}},
	Title = {Th.pl},
	Year = {2009}}

@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{\c c}ois Lamarche and Charles Stewart},
	Keywords = {deep inference},
	Note = {ICALP Workshop. ISSN 1430-211X. \url{http://cs.bath.ac.uk/pb/SD05/SD05-Proc.pdf}},
	Pages = {35--52},
	Publisher = {Technische Universit{\"a}t Dresden},
	Title = {The Three Dimensions of Proofs},
	Year = 2005}

@article{Guir:06:The-Thre:qt,
	Author = {Guiraud, Yves},
	Date-Modified = {2006-09-13 07:28:32 +0100},
	Journal = {Annals of Pure and Applied Logic},
	Keywords = {deep inference},
	Note = {\url{http://www.loria.fr/~guiraudy/recherche/cos1.pdf}},
	Number = {1-2},
	Pages = {266--295},
	Title = {The Three Dimensions of Proofs},
	Volume = {141},
	Year = {2006}}

@phdthesis{Gund:09:A-Genera:kx,
	Author = {Gundersen, Tom},
	Date-Added = {2009-08-09 11:17:28 +0200},
	Date-Modified = {2010-08-20 19:03:35 +0200},
	Keywords = {deep inference},
	Note = {\url{http://tel.archives-ouvertes.fr/docs/00/50/92/41/PDF/thesis.pdf}},
	School = {University of Bath},
	Title = {A General View of Normalisation Through Atomic Flows},
	Year = {2009}}

@inproceedings{GundHeijPari:13:Atomic-L:fk,
	Author = {Gundersen, Tom and Heijltjes, Willem and Parigot, Michel},
	Booktitle = {28th Annual IEEE Symposium on Logic in Computer Science (LICS)},
	Date-Added = {2013-03-23 11:39:59 +0000},
	Date-Modified = {2013-03-23 11:45:02 +0000},
	Keywords = {deep inference},
	Note = {In press.},
	Publisher = {IEEE},
	Title = {Atomic Lambda Calculus: {A} Typed Lambda-Calculus with Explicit Sharing},
	Year = {2013}}

@mastersthesis{Hein:05:Geometri:bs,
	Author = {Hein, Robert},
	Date-Modified = {2006-07-13 13:12:56 +0100},
	Keywords = {deep inference},
	Note = {\url{http://bitschnitzer.de/robert_thesis.ps.gz}},
	School = {Technische Universit{\"a}t Dresden},
	Title = {Geometric Theories and Modal Logic in the Calculus of Structures},
	Year = 2005}

@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{\c c}ois Lamarche and Charles Stewart},
	Keywords = {deep inference},
	Note = {ICALP Workshop. ISSN 1430-211X. \url{http://cs.bath.ac.uk/pb/SD05/SD05-Proc.pdf}},
	Pages = {126--143},
	Publisher = {Technische Universit{\"a}t Dresden},
	Title = {Purity Through Unravelling},
	Year = 2005}

@mastersthesis{Hors:06:The-Logi:fk,
	Author = {Horsfall, Benjamin Robert},
	Date-Added = {2007-09-08 07:07:08 +0100},
	Date-Modified = {2007-09-08 07:09:21 +0100},
	Keywords = {deep inference},
	Note = {\url{http://www.cs.mu.oz.au/~horsfall/horsfall-mcs.pdf}},
	School = {University of Melbourne},
	Title = {The Logic of Bunched Implications: {A} Memoir},
	Year = {2006}}

@unpublished{Hugh:04:Deep-Inf:fc,
	Author = {Hughes, Dominic J.D.},
	Date-Modified = {2006-07-13 13:12:55 +0100},
	Keywords = {deep inference},
	Note = {\url{http://boole.stanford.edu/~dominic/papers/di/di.pdf}},
	Title = {Deep Inference Proof Theory Equals Categorical Proof Theory Minus Coherence},
	Year = 2004}

@article{Japa:07:Cirquent:fk,
	Author = {Japaridze, Giorgi},
	Date-Added = {2007-09-22 14:52:39 +0100},
	Date-Modified = {2008-12-03 15:13:05 +0100},
	Journal = {Journal of Logic and Computation},
	Keywords = {deep inference},
	Note = {\url{http://arxiv.org/pdf/0709.1308}},
	Number = {6},
	Pages = {983--1028},
	Title = {Cirquent Calculus Deepened},
	Volume = {18},
	Year = {2008}}

@article{Jera::On-the-C:kx,
	Author = {Je{\v r}{\'a}bek, Emil},
	Date-Added = {2007-12-02 20:34:04 +0000},
	Date-Modified = {2012-07-12 16:06:02 +0100},
	Journal = {Journal of Logic and Computation},
	Keywords = {deep inference},
	Note = {\url{http://www.math.cas.cz/~jerabek/papers/cos.pdf}},
	Number = {2},
	Pages = {323--339},
	Title = {Proof Complexity of the Cut-Free Calculus of Structures},
	Volume = {19},
	Year = {2009}}

@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{\c c}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'. \url{http://cs.bath.ac.uk/pb/SD05/SD05-Proc.pdf}},
	Pages = {81--94},
	Publisher = {Technische Universit{\"a}t Dresden},
	Title = {Completeness of {MLL} Proof-nets w.r.t.\ Weak Distributivity},
	Year = 2005}

@article{Join:07:Complete:uq,
	Author = {Joinet, Jean-Baptiste},
	Date-Modified = {2007-12-02 19:43:45 +0000},
	Journal = {The Journal of Symbolic Logic},
	Keywords = {deep inference},
	Note = {\url{http://www-philo.univ-paris1.fr/Joinet/joinetJSLmain.pdf}},
	Number = {1},
	Pages = {159--170},
	Title = {Completeness of {MLL} Proof-nets w.r.t.\ Weak Distributivity},
	Volume = {72},
	Year = 2007}

@inproceedings{KahrMoreReil:05:Implemen:wb,
	Author = {Kahramano{\u g}ullar{\i}, Ozan and Moreau, Pierre-Etienne and Reilles, Antoine},
	Booktitle = {Structures and Deduction},
	Date-Modified = {2007-09-18 10:54:00 +0100},
	Editor = {Paola Bruscoli and Fran{\c c}ois Lamarche and Charles Stewart},
	Keywords = {deep inference},
	Note = {ICALP Workshop. ISSN 1430-211X. \url{http://www.wv.inf.tu-dresden.de/~guglielm/ok/sd05.pdf}},
	Pages = {158--172},
	Publisher = {Technische Universit{\"a}t Dresden},
	Title = {Implementing Deep Inference in {TOM}},
	Year = 2005}

@inproceedings{Kahr:04:Implemen:ct,
	Address = {Universit\'e Henri Poincar\'e, Nancy, France},
	Author = {Kahramano{\u g}ullar{\i}, Ozan},
	Booktitle = {ESSLLI 2004 Student Session},
	Date-Modified = {2010-07-17 18:33:19 +0200},
	Keywords = {deep inference},
	Note = {16th European Summer School in Logic, Language and Information. \url{http://www.wv.inf.tu-dresden.de/~guglielm/ok/esslli04.pdf}},
	Pages = {117--127},
	Title = {Implementing System {BV} of the Calculus of Structures in {M}aude},
	Year = 2004}

@unpublished{Kahr:08:Ingredie:bf,
	Author = {Kahramano{\u g}ullar{\i}, Ozan},
	Date-Added = {2008-07-01 11:55:42 +0100},
	Date-Modified = {2008-07-01 12:11:31 +0100},
	Keywords = {deep inference},
	Note = {Short paper at CL\&C'08. \url{http://www.wv.inf.tu-dresden.de/~guglielm/ok/ingredients.pdf}},
	Title = {Ingredients of a Deep Inference Theorem Prover},
	Year = {2008}}

@unpublished{Kahr:08:Interact:ad,
	Author = {Kahramano{\u g}ullar{\i}, Ozan},
	Date-Added = {2008-07-01 11:53:32 +0100},
	Date-Modified = {2008-07-01 12:03:59 +0100},
	Keywords = {deep inference},
	Note = {\url{http://www.wv.inf.tu-dresden.de/~guglielm/ok/id.pdf}},
	Title = {Interaction and Depth Against Nondeterminism in Deep Inference Proof Search},
	Year = {2008}}

@unpublished{Kahr::Labelled:ri,
	Author = {Kahramano{\u g}ullar{\i}, Ozan},
	Date-Modified = {2007-09-18 11:20:15 +0100},
	Keywords = {deep inference},
	Note = {Presented at the 1st World Congress on Universal Logic. \url{http://www.wv.inf.tu-dresden.de/~guglielm/ok/unilog.pdf}},
	Title = {Labeled Event Structure Semantics of Linear Logic Planning}}

@inproceedings{Kahr:07:Maude-as:lr,
	Author = {Kahramano{\u g}ullar{\i}, Ozan},
	Booktitle = {Eighth International Workshop on Rule Based Programming (RULE 2007)},
	Date-Added = {2007-06-26 09:53:26 +0100},
	Date-Modified = {2010-07-17 18:32:57 +0200},
	Editor = {J. Visser and V. Winter},
	Keywords = {deep inference},
	Note = {\url{http://www.wv.inf.tu-dresden.de/~guglielm/ok/rule07.pdf}},
	Pages = {35--50},
	Publisher = {Elsevier},
	Series = {Electronic Notes in Theoretical Computer Science},
	Title = {Maude as a Platform for Designing and Implementing Deep Inference Systems},
	Volume = {219},
	Year = {2008}}

@phdthesis{Kahr:06:Nondeter:fk,
	Author = {Kahramano{\u g}ullar{\i}, Ozan},
	Date-Added = {2007-08-13 18:00:14 +0200},
	Date-Modified = {2007-08-13 18:01:55 +0200},
	Keywords = {deep inference},
	Note = {\url{http://www.wv.inf.tu-dresden.de/~guglielm/ok/ozansthesis.pdf}},
	School = {Technische Universit{\"a}t Dresden},
	Title = {Nondeterminism and Language Design in Deep Inference},
	Year = {2006}}

@article{Kahr:09:On-Linea:ix,
	Author = {Kahramano{\u g}ullar{\i}, Ozan},
	Date-Added = {2009-01-24 06:35:50 +0100},
	Date-Modified = {2009-10-16 08:35:36 +0200},
	Journal = {Information and Computation},
	Keywords = {deep inference},
	Note = {\url{http://www.sciencedirect.com/science/article/pii/S089054010900073X}},
	Number = {11},
	Pages = {1229--1258},
	Publisher = {Elsevier},
	Title = {On Linear Logic Planning and Concurrency},
	Volume = {207},
	Year = {2009}}

@inproceedings{Kahr:08:On-Linea:fk,
	Author = {Kahramano{\u g}ullar{\i}, Ozan},
	Booktitle = {Language and Automata Theory and Applications},
	Date-Added = {2008-01-20 08:23:25 +0000},
	Date-Modified = {2009-01-24 06:25:18 +0100},
	Editor = {Mart{\'\i}n-Vide, Carlos and Otto, Friedrich and Fernau, Henning},
	Keywords = {deep inference},
	Note = {\url{http://www.wv.inf.tu-dresden.de/~guglielm/ok/lata.pdf}},
	Pages = {250--262},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {On Linear Logic Planning and Concurrency},
	Volume = {5196},
	Year = {2008}}

@unpublished{Kahr:04:A-New-Lo:fk,
	Author = {Kahramano{\u g}ullar{\i}, Ozan},
	Date-Added = {2007-09-08 08:31:48 +0100},
	Date-Modified = {2012-07-05 09:09:13 +0100},
	Keywords = {deep inference},
	Note = {Short paper at LPAR 2007.},
	Title = {On Linear Logic Planning and Concurrency},
	Year = {2007}}

@inproceedings{Kahr:06:Reducing:hc,
	Author = {Kahramano{\u g}ullar{\i}, Ozan},
	Booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)},
	Date-Modified = {2011-12-29 09:36:33 +0000},
	Editor = {Hermann, Miki and Voronkov, Andrei},
	Keywords = {deep inference},
	Note = {\url{http://dx.doi.org/10.1007/11916277_19}},
	Pages = {272--286},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {Reducing Nondeterminism in the Calculus of Structures},
	Volume = {4246},
	Year = 2006}

@article{Kahr:07:System-B:fk,
	Author = {Kahramano{\u g}ullar{\i}, Ozan},
	Date-Added = {2007-03-24 13:01:58 +0000},
	Date-Modified = {2009-05-19 10:01:24 +0200},
	Journal = {Annals of Pure and Applied Logic},
	Keywords = {deep inference},
	Note = {\url{http://dx.doi.org/10.1016/j.apal.2007.11.005}},
	Number = {1--3},
	Pages = {107--121},
	Title = {System {BV} Is {NP}-Complete},
	Volume = {152},
	Year = {2007}}

@inproceedings{Kahr:06:System-B:ht,
	Author = {Kahramano{\u g}ullar{\i}, Ozan},
	Booktitle = {12th Workshop on Logic, Language, Information and Computation (WoLLIC)},
	Date-Modified = {2011-12-29 09:22:45 +0000},
	Editor = {de Queiroz, Ruy and Macintyre, Angus and Bittencourt, Guilherme},
	Keywords = {deep inference},
	Note = {\url{http://www.wv.inf.tu-dresden.de/~guglielm/ok/BVnpc.pdf}},
	Pages = {87--99},
	Publisher = {Elsevier},
	Series = {Electronic Notes in Theoretical Computer Science},
	Title = {System {BV} Is {NP}-Complete},
	Volume = {143},
	Year = {2006}}

@inproceedings{Kahr:04:System-B:dg,
	Author = {Kahramano{\u g}ullar{\i}, Ozan},
	Booktitle = {19th International Symposium on Computer and Information Sciences, ISCIS 2004},
	Date-Modified = {2007-09-18 10:48:04 +0100},
	Editor = {C. Aykanat and T. Dayar and I. K{\"o}rpeo{\u g}lu},
	Keywords = {deep inference},
	Note = {\url{http://www.wv.inf.tu-dresden.de/~guglielm/ok/bvn.pdf}},
	Pages = {986--995},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {System {BV} without the Equalities for Unit},
	Volume = 3280,
	Year = 2004}

@inproceedings{Kahr:05:Towards-:uz,
	Author = {Kahramano{\u g}ullar{\i}, Ozan},
	Booktitle = {The IASTED International Conference on Artificial Intelligence and Applications, AIA 2005},
	Date-Modified = {2007-09-18 10:48:19 +0100},
	Keywords = {deep inference},
	Note = {\url{http://www.wv.inf.tu-dresden.de/~guglielm/ok/aia05.pdf}},
	Title = {Towards Planning as Concurrency},
	Year = 2005}

@inproceedings{LamaStra:05:Construc:qq,
	Author = {Lamarche, Fran{\c c}ois and Stra{\ss}burger, Lutz},
	Booktitle = {20th Annual IEEE Symposium on Logic in Computer Science (LICS)},
	Date-Modified = {2011-12-29 09:22:28 +0000},
	Editor = {Panangaden, Prakash},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/FreeBool-long.pdf}},
	Pages = {209--218},
	Publisher = {IEEE},
	Title = {Constructing Free Boolean Categories},
	Year = 2005}

@article{Lama::Explorin:mw,
	Author = {Lamarche, Fran{\c c}ois},
	Date-Added = {2006-06-11 12:09:02 +0100},
	Date-Modified = {2007-12-02 23:20:40 +0000},
	Journal = {Theory and Applications of Categories},
	Keywords = {deep inference},
	Note = {\url{http://www.loria.fr/~lamarche/papers/Gap.pdf}},
	Number = {17},
	Pages = {473--535},
	Title = {Exploring the Gap between Linear and Classical Logic},
	Volume = {18},
	Year = {2007}}

@article{LamaStra:06:From-Pro:et,
	Author = {Lamarche, Fran{\c c}ois and Stra{\ss}burger, Lutz},
	Date-Modified = {2006-10-06 11:20:46 +0100},
	Journal = {Logical Methods in Computer Science},
	Keywords = {deep inference},
	Note = {\url{http://arxiv.org/pdf/cs.LO/0605054}},
	Number = {4},
	Pages = {3:1--44},
	Title = {From Proof Nets to the Free *-Autonomous Category},
	Volume = {2},
	Year = {2006}}

@inproceedings{LamaStra:05:Naming-P:ov,
	Author = {Lamarche, Fran{\c c}ois and Stra{\ss}burger, Lutz},
	Booktitle = {Typed Lambda Calculi and Applications (TLCA)},
	Date-Modified = {2011-12-29 09:22:20 +0000},
	Editor = {Pawe{\l} Urzyczyn},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/namingproofsCL.pdf}},
	Pages = {246--261},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {Naming Proofs in Classical Propositional Logic},
	Volume = 3461,
	Year = 2005}

@unpublished{LengBrun:05:Getting-:fk,
	Author = {Lengrand, St{\'e}phane and Br{\"u}nnler, Kai},
	Date-Added = {2007-10-06 06:46:17 +0100},
	Date-Modified = {2007-10-06 07:17:11 +0100},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lengrand/Work/Reports/DI.ps}},
	Title = {Getting Formalisms {A} and {B} by Proof-Terms and Typing Systems},
	Year = {2005}}

@phdthesis{Leng:06:Normalis:uq,
	Author = {Lengrand, St{\'e}phane},
	Date-Added = {2007-10-06 07:11:08 +0100},
	Date-Modified = {2007-10-06 07:15:24 +0100},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lengrand/Work/Reports/MyThesis.pdf}},
	School = {Universit{\'e} Paris VII - Denis Diderot, University of St Andrews},
	Title = {Normalisation \& Equivalence in Proof Theory \& Type Theory},
	Year = {2006}}

@phdthesis{Mrm-:06:Categori:ff,
	Author = {McKinley, Richard},
	Date-Added = {2006-03-18 10:08:56 +0000},
	Date-Modified = {2008-03-27 13:54:57 +0000},
	Keywords = {deep inference},
	Note = {\url{http://www.cs.bath.ac.uk/~csprim/thesis.pdf}},
	School = {University of Bath},
	Title = {Categorical Models of First Order Classical Proofs},
	Year = {2006}}

@inproceedings{Mrm-:05:Classica:ye,
	Author = {McKinley, Richard},
	Booktitle = {Structures and Deduction},
	Date-Modified = {2008-03-27 13:54:57 +0000},
	Editor = {Paola Bruscoli and Fran{\c c}ois Lamarche and Charles Stewart},
	Keywords = {deep inference},
	Note = {ICALP Workshop. ISSN 1430-211X. \url{http://www.cs.bath.ac.uk/~csprim/csl05.pdf}},
	Pages = {19--33},
	Publisher = {Technische Universit{\"a}t Dresden},
	Title = {Classical Categories and Deep Inference},
	Year = 2005}

@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 = {2011-12-29 09:21:43 +0000},
	Editor = {Ono, Hiroakira and Kanazawa, Makoto and de Queiroz, Ruy},
	Keywords = {deep inference},
	Note = {\url{http://users.cecs.anu.edu.au/~linda/postniece-dbi.pdf}},
	Pages = {320--334},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {Deep Inference in Bi-intuitionistic Logic},
	Volume = {5514},
	Year = {2009}}

@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},
	Note = {\url{http://users.cecs.anu.edu.au/~linda/thesis.pdf}},
	School = {The Australian National University},
	Title = {Proof Theory and Proof Search of Bi-Intuitionistic and Tense Logic},
	Year = {2011}}

@inproceedings{Reil:06:Canonica:fe,
	Author = {Reilles, Antoine},
	Booktitle = {6th International Workshop on Rewriting Logic and Its Applications},
	Date-Added = {2006-03-28 18:48:42 +0100},
	Date-Modified = {2009-03-22 15:34:48 +0100},
	Keywords = {deep inference},
	Note = {\url{http://arxiv.org/pdf/cs.PL/0601019}},
	Pages = {165--179},
	Publisher = {Elsevier},
	Series = {Electronic Notes in Theoretical Computer Science},
	Title = {Canonical Abstract Syntax Trees},
	Volume = {176},
	Year = {2007}}

@unpublished{Rove:12:Communic:kx,
	Author = {Roversi, Luca},
	Date-Added = {2013-03-07 14:28:39 +0000},
	Date-Modified = {2013-03-07 14:35:23 +0000},
	Keywords = {deep inference},
	Note = {\url{http://arxiv.org/pdf/1212.4669v1.pdf}},
	Title = {Communication, and Concurrency with Logic-Based Restriction Inside a Calculus of Structures},
	Year = {2012}}

@unpublished{Rove:12:Extendin:uq,
	Author = {Roversi, Luca},
	Date-Added = {2013-03-07 14:14:31 +0000},
	Date-Modified = {2013-03-07 14:15:59 +0000},
	Keywords = {deep inference},
	Note = {\url{http://arxiv.org/pdf/1212.4483v1.pdf}},
	Title = {Extending a System in the Calculus of Structures with a Self-Dual Quantifier},
	Year = {2012}}

@inproceedings{Rove:11:Linear-L:kx,
	Author = {Roversi, Luca},
	Booktitle = {Typed Lambda Calculi and Applications},
	Date-Added = {2011-05-04 18:35:05 +0100},
	Date-Modified = {2011-05-04 18:37:10 +0100},
	Editor = {Ong, Luke},
	Keywords = {deep inference},
	Note = {\url{http://www.di.unito.it/~rover/RESEARCH/PUBLICATIONS/2011-TLCA/Roversi2011TLCA.pdf}},
	Pages = {184--197},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {Linear Lambda Calculus and Deep Inference},
	Volume = {6690},
	Year = {2011}}

@unpublished{Rove::Linear-L:fk,
	Author = {Roversi, Luca},
	Date-Added = {2010-11-28 16:09:08 +0000},
	Date-Modified = {2011-01-25 16:45:22 +0000},
	Keywords = {deep inference},
	Note = {\url{http://arxiv.org/pdf/1011.3668}},
	Title = {Linear Lambda Calculus with Explicit Substitutions as Proof-Search in Deep Inference}}

@inproceedings{StewStou:05:A-System:tg,
	Author = {Stewart, Charles and Stouppa, Phiniki},
	Booktitle = {Advances in Modal Logic},
	Date-Modified = {2006-09-07 11:10:13 +0100},
	Editor = {Renate Schmidt and Ian Pratt-Hartmann and Mark Reynolds and Heinrich Wansing},
	Keywords = {deep inference},
	Note = {\url{http://www.aiml.net/volumes/volume5/Stewart.ps}},
	Pages = {309--333},
	Publisher = {King's College Publications},
	Title = {A Systematic Proof Theory for Several Modal Logics},
	Volume = 5,
	Year = 2005}

@article{Stou:06:A-Deep-I:rt,
	Author = {Stouppa, Phiniki},
	Date-Modified = {2011-05-06 19:34:22 +0100},
	Journal = {Studia Logica},
	Keywords = {deep inference},
	Note = {\url{http://www.iam.unibe.ch/tilpub/2007/sto07.pdf}},
	Number = {2},
	Pages = {199--214},
	Title = {A Deep Inference System for the Modal Logic {S5}},
	Volume = {85},
	Year = {2007}}

@mastersthesis{Stou:04:The-Desi:vg,
	Author = {Stouppa, Phiniki},
	Date-Modified = {2008-01-28 14:42:34 +0000},
	Keywords = {deep inference},
	Note = {\url{http://www.wv.inf.tu-dresden.de/Publications/Diploma/diplom_stouppa.pdf}},
	School = {Technische Universit{\"a}t Dresden},
	Title = {The Design of Modal Proof Theories: The case of {S5}},
	Year = 2004}

@inproceedings{Stra:07:A-Charac:fk,
	Author = {Stra{\ss}burger, Lutz},
	Booktitle = {Term Rewriting and Applications---18th International Conference, RTA},
	Date-Modified = {2010-07-17 18:52:57 +0200},
	Editor = {Baader, Franz},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/CharMedial.pdf}},
	Pages = {344--358},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {A Characterisation of Medial as Rewriting Rule},
	Volume = {4533},
	Year = 2007}

@techreport{Stra:02:A-Local-:ve,
	Author = {Stra{\ss}burger, Lutz},
	Date-Modified = {2006-07-13 13:12:54 +0100},
	Institution = {Technische Universit{\"a}t Dresden},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/lls.pdf}},
	Number = {WV-02-01},
	Title = {A Local System for Linear Logic},
	Year = 2002}

@inproceedings{Stra:02:A-Local-:ul,
	Author = {Stra{\ss}burger, Lutz},
	Booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)},
	Date-Modified = {2011-12-29 09:36:19 +0000},
	Editor = {Baaz, Matthias and Voronkov, Andrei},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/lls-lpar.pdf}},
	Pages = {388--402},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {A Local System for Linear Logic},
	Volume = 2514,
	Year = 2002}

@article{StraGugl:09:A-System:vn,
	Author = {Stra{\ss}burger, Lutz and Guglielmi, Alessio},
	Date-Added = {2009-03-30 09:16:04 +0200},
	Date-Modified = {2011-10-31 11:39:08 +0000},
	Journal = {ACM Transactions on Computational Logic},
	Keywords = {deep inference},
	Note = {\url{http://arxiv.org/pdf/0903.5259}},
	Number = {4},
	Pages = {23:1--39},
	Title = {A System of Interaction and Structure {IV}: {T}he Exponentials and Decomposition},
	Volume = {12},
	Year = {2011}}

@inproceedings{Stra:12:Nested-S:uq,
	Author = {Stra{\ss}burger, Lutz},
	Booktitle = {FoSSaCS},
	Date-Added = {2012-07-07 13:24:04 +0100},
	Date-Modified = {2013-03-05 18:43:41 +0000},
	Keywords = {deep inference},
	Note = {In press. \url{http://www.lix.polytechnique.fr/~lutz/papers/nested-int-mod-fossacs13.pdf}},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {Cut Elimination in Nested Sequents for Intuitionistic Modal Logics},
	Year = {2013}}

@inproceedings{Stra:07:Deep-Inf:uq,
	Author = {Stra{\ss}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{\o}rgen Villadsen and Thomas Bolander and Torben Bra{\"u}ner},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/hybrid.pdf}},
	Pages = {13--22},
	Title = {Deep Inference for Hybrid Logic},
	Year = {2007}}

@article{Stra:08:Extensio:kk,
	Author = {Stra{\ss}burger, Lutz},
	Date-Added = {2008-07-01 11:58:02 +0100},
	Date-Modified = {2012-09-03 00:26:13 +0100},
	Journal = {Annals of Pure and Applied Logic},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/psppp.pdf}},
	Number = {12},
	Pages = {1995--2007},
	Title = {Extension Without Cut},
	Volume = {163},
	Year = {2012}}

@inproceedings{Stra:05:From-Dee:yb,
	Author = {Stra{\ss}burger, Lutz},
	Booktitle = {Structures and Deduction},
	Date-Modified = {2009-09-03 09:01:47 +0200},
	Editor = {Paola Bruscoli and Fran{\c c}ois Lamarche and Charles Stewart},
	Keywords = {deep inference},
	Note = {ICALP Workshop. ISSN 1430-211X. \url{http://www.lix.polytechnique.fr/~lutz/papers/deepnet-SD05.pdf}},
	Pages = {2--18},
	Publisher = {Technische Universit{\"a}t Dresden},
	Title = {From Deep Inference to Proof Nets},
	Year = 2005}

@article{Stra:09:From-Dee:fr,
	Author = {Stra{\ss}burger, Lutz},
	Date-Added = {2009-09-03 08:25:28 +0200},
	Date-Modified = {2011-09-05 17:32:22 +0100},
	Journal = {Journal of Logic and Computation},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/deepnet.pdf}},
	Number = {4},
	Pages = {589--624},
	Title = {From Deep Inference to Proof Nets via Cut Elimination},
	Volume = {21},
	Year = 2011}

@phdthesis{Stra:03:Linear-L:lp,
	Author = {Stra{\ss}burger, Lutz},
	Date-Modified = {2006-07-13 13:12:57 +0100},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/dissvonlutz.pdf}},
	School = {Technische Universit{\"a}t Dresden},
	Title = {Linear Logic and Noncommutativity in the Calculus of Structures},
	Year = 2003}

@article{Stra:03:MELL-in-:oy,
	Author = {Stra{\ss}burger, Lutz},
	Date-Modified = {2006-07-13 13:12:57 +0100},
	Journal = {Theoretical Computer Science},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/els.pdf}},
	Pages = {213--285},
	Title = {{MELL} in the Calculus of Structures},
	Volume = 309,
	Year = 2003}

@inproceedings{StraLama:04:On-Proof:ec,
	Author = {Stra{\ss}burger, Lutz and Lamarche, Fran{\c c}ois},
	Booktitle = {Computer Science Logic (CSL)},
	Date-Modified = {2011-12-29 09:32:24 +0000},
	Editor = {J. Marcinkowski and A. Tarlecki},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/multPN.pdf}},
	Pages = {145--159},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {On Proof Nets for Multiplicative Linear Logic with Units},
	Volume = 3210,
	Year = 2004}

@article{Stra:06:On-the-A:jy,
	Author = {Stra{\ss}burger, Lutz},
	Date-Modified = {2012-03-25 22:00:21 +0100},
	Journal = {Theory and Applications of Categories},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/medial.pdf}},
	Number = {18},
	Pages = {536--601},
	Title = {On the Axiomatisation of Boolean Categories with and Without Medial},
	Volume = {18},
	Year = 2007}

@techreport{Stra:06:Proof-Ne:fk,
	Author = {Stra{\ss}burger, Lutz},
	Date-Added = {2007-10-10 11:01:54 +0100},
	Date-Modified = {2008-03-23 18:21:43 +0000},
	Institution = {INRIA},
	Keywords = {deep inference},
	Note = {\url{http://hal.inria.fr/docs/00/11/43/20/PDF/RR-6013.pdf}},
	Number = {6013},
	Title = {Proof Nets and the Identity of Proofs},
	Year = {2006}}

@inproceedings{Strasburger:2008qf,
	Author = {Stra{\ss}burger, Lutz},
	Booktitle = {Typed Lambda Calculi and Applications (TLCA)},
	Date-Added = {2008-05-19 11:32:46 +0100},
	Date-Modified = {2011-12-29 09:21:09 +0000},
	Editor = {Curien, Pierre-Louis},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/ObsPT-MLL2-finalforTLCA09.pdf}},
	Pages = {309--324},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic},
	Volume = {5608},
	Year = 2009}

@inproceedings{Stra:03:System-N:mb,
	Author = {Stra{\ss}burger, Lutz},
	Booktitle = {10th Workshop on Logic, Language, Information and Computation (WoLLIC)},
	Date-Added = {2007-03-29 10:00:53 +0100},
	Date-Modified = {2007-03-29 10:00:53 +0100},
	Editor = {De Queiroz, Ruy and Pimentel, Elaine and Figueiredo, Luc{\'\i}lia},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/NELundec_wollic03.pdf}},
	Publisher = {Elsevier},
	Series = {Electronic Notes in Theoretical Computer Science},
	Title = {System {NEL} Is Undecidable},
	Volume = 84,
	Year = 2003}

@techreport{Stra:03:The-Unde:gn,
	Author = {Stra{\ss}burger, Lutz},
	Date-Modified = {2006-07-13 13:12:59 +0100},
	Institution = {Technische Universit{\"a}t Dresden},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/NELundeci.pdf}},
	Number = {WV-03-05},
	Title = {The Undecidability of System {NEL}},
	Year = 2003}

@unpublished{Stra:11:Towards-:fk,
	Author = {Stra{\ss}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. \url{http://www.lix.polytechnique.fr/~lutz/papers/HDR.pdf}},
	School = {Universit{\'e} Paris VII - Denis Diderot},
	Title = {Towards a Theory of Proofs of Classical Logic},
	Year = {2011}}

@unpublished{Stra:06:What-Cou:vh,
	Author = {Stra{\ss}burger, Lutz},
	Date-Added = {2006-07-03 07:43:21 +0100},
	Date-Modified = {2006-07-13 13:12:59 +0100},
	Keywords = {deep inference},
	Note = {Accepted by Cl\&C '06. \url{http://www.lix.polytechnique.fr/~lutz/papers/medial-kurz.pdf}},
	Title = {What Could a Boolean Category Be?},
	Year = 2006}

@incollection{Stra:05:What-Is-:wl,
	Author = {Stra{\ss}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},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/WhatLogicProof.pdf}},
	Pages = {135--152},
	Publisher = {Birkh{\"a}user},
	Title = {What Is a Logic, and What Is a Proof?},
	Year = 2007}

@inproceedings{Stra:10:What-Is-:fk,
	Author = {Stra{\ss}burger, Lutz},
	Booktitle = {Programs, Proofs, Processes---6th Conference on Computability in Europe},
	Date-Added = {2010-07-17 18:29:43 +0200},
	Date-Modified = {2010-07-17 18:43:41 +0200},
	Editor = {Ferreira, Fernando and L{\"o}we, Benedikt and Mayordomo, Elvira and Mendes Gomes, Lu{\'\i}s},
	Keywords = {deep inference},
	Note = {\url{http://www.lix.polytechnique.fr/~lutz/papers/CiE10.pdf}},
	Pages = {406--416},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {What Is the Problem with Proof Nets for Classical Logic?},
	Volume = {6158},
	Year = {2010}}

@inproceedings{Tiu:06:A-Local-:gf,
	Author = {Tiu, Alwen},
	Booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)},
	Date-Modified = {2011-12-29 09:36:25 +0000},
	Editor = {Hermann, Miki and Voronkov, Andrei},
	Keywords = {deep inference},
	Note = {\url{http://users.cecs.anu.edu.au/~tiu/localint.pdf}},
	Pages = {242--256},
	Publisher = {Springer-Verlag},
	Series = {Lecture Notes in Computer Science},
	Title = {A Local System for Intuitionistic Logic},
	Volume = {4246},
	Year = {2006}}

@article{Tiu:06:A-System:ai,
	Author = {Tiu, Alwen},
	Date-Modified = {2011-10-20 18:18:53 +0100},
	Journal = {Logical Methods in Computer Science},
	Keywords = {deep inference},
	Note = {\url{http://arxiv.org/pdf/cs.LO/0512036}},
	Number = {2},
	Pages = {4:1--24},
	Title = {A System of Interaction and Structure {II}: {T}he Need for Deep Inference},
	Volume = {2},
	Year = {2006}}

@inproceedings{TiuIanoGore:12:Grammar-:uq,
	Author = {Tiu, Alwen and Ianovski, Egor and Gor{\'e}, Rajeev},
	Booktitle = {Advances in Modal Logic},
	Date-Added = {2012-07-08 16:35:55 +0100},
	Date-Modified = {2013-03-05 19:34:37 +0000},
	Editor = {Bolander, Thomas and Bra{\"u}ner, Torben and Ghilardi, Silvio and Lawrence Moss},
	Keywords = {deep inference},
	Note = {\url{http://users.cecs.anu.edu.au/~tiu/papers/grammar.pdf}},
	Pages = {516--537},
	Publisher = {College Publications},
	Title = {Grammar Logics in Nested Sequent Calculus: {P}roof Theory and Decision Procedures},
	Volume = {9},
	Year = {2012}}

@techreport{Tiu:01:A1-Unifi:ij,
	Author = {Tiu, Alwen Fernanto},
	Date-Modified = {2006-07-13 13:12:54 +0100},
	Institution = {Technische Universit{\"a}t Dresden},
	Keywords = {deep inference},
	Note = {\url{http://users.cecs.anu.edu.au/~tiu/a1.ps.gz}},
	Number = {WV-01-08},
	Title = {{A1}-Unification},
	Year = 2001}

@techreport{Tiu:01:Combinin:qf,
	Author = {Tiu, Alwen Fernanto},
	Date-Modified = {2006-07-13 13:12:55 +0100},
	Institution = {Technische Universit{\"a}t Dresden},
	Keywords = {deep inference},
	Note = {\url{http://users.cecs.anu.edu.au/~tiu/comb4.ps.gz}},
	Number = {WV-01-09},
	Title = {Combining {A1}- and {AC1}-Unification Sharing Unit},
	Year = 2001}

@techreport{Tiu:01:Properti:zk,
	Author = {Tiu, Alwen Fernanto},
	Date-Modified = {2006-07-13 13:12:58 +0100},
	Institution = {Technische Universit{\"a}t Dresden},
	Keywords = {deep inference},
	Note = {\url{http://users.cecs.anu.edu.au/~tiu/thesisc.pdf}},
	Number = {WV-01-06},
	Title = {Properties of a Logical System in the Calculus of Structures},
	Year = 2001}