@inproceedings(acc:hor:str:LBF, author = {Matteo Acclavio and Ross Horne and Stra{\ss}burger, Lutz}, year = {2020}, title = {Logic beyond formulas: a proof system on graphs}, booktitle = {35th Annual ACM/IEEE Symposium on Logic in Computer Science, {LICS}'20}, publisher = {{ACM}}, pages = {38--52}, doi = {10.1145/3373718.3394763}, ) @inproceedings(brunnler:tiu:01, author = {Kai Br{\"u}nnler and Alwen Fernanto Tiu}, year = {2001}, title = {A Local System for Classical Logic}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning , 8th International Conference, {LPAR} 2001}, series = {Lecture Notes in Computer Science}, volume = {2250}, publisher = {Springer}, pages = {347--361}, doi = {10.1007/3-540-45653-8\_24}, ) @article(Carvalho18, author = {Daniel de Carvalho}, year = {2018}, title = {Taylor expansion in linear logic is invertible}, journal = {Log. Methods Comput. Sci.}, volume = {14}, number = {4}, doi = {10.23638/LMCS-14(4:21)2018}, ) @article(Ehrhard05, author = {Thomas Ehrhard}, year = {2005}, title = {Finiteness spaces}, journal = {Mathematical Structures in Computer Science}, volume = {15}, number = {4}, pages = {615--646}, doi = {10.1017/S0960129504004645}, ) @article(Ehrhard18, author = {Thomas Ehrhard}, year = {2018}, title = {An introduction to differential linear logic: proof-nets, models and antiderivatives}, journal = {Mathematical Structures in Computer Science}, volume = {28}, number = {7}, pages = {995--1060}, doi = {10.1017/S0960129516000372}, ) @article(EhrhardLaurent10, author = {Thomas Ehrhard and Olivier Laurent}, year = {2010}, title = {Interpreting a finitary pi-calculus in differential interaction nets}, journal = {Inf. Comput.}, volume = {208}, number = {6}, pages = {606--633}, doi = {10.1016/j.ic.2009.06.005}, ) @article(EhrhardRegnier03, author = {Thomas Ehrhard and Laurent Regnier}, year = {2003}, title = {The differential lambda-calculus}, journal = {Theor. Comput. Sci.}, volume = {309}, number = {1-3}, pages = {1--41}, doi = {10.1016/S0304-3975(03)00392-X}, ) @inproceedings(EhrhardRegnier06b, author = {Thomas Ehrhard and Laurent Regnier}, year = {2006}, title = {B{\"{o}}hm Trees, Krivine's Machine and the Taylor Expansion of Lambda-Terms}, booktitle = {Second Conference on Computability in Europe, CiE 2006}, series = {Lecture Notes in Computer Science}, volume = {3988}, publisher = {Springer}, pages = {186--197}, doi = {10.1007/11780342\_20}, ) @article(EhrhardRegnier06, author = {Thomas Ehrhard and Laurent Regnier}, year = {2006}, title = {Differential interaction nets}, journal = {Theor. Comput. Sci.}, volume = {364}, number = {2}, pages = {166--195}, doi = {10.1016/j.tcs.2006.08.003}, ) @article(EhrhardRegnier08, author = {Thomas Ehrhard and Laurent Regnier}, year = {2008}, title = {Uniformity and the Taylor expansion of ordinary lambda-terms}, journal = {Theor. Comput. Sci.}, volume = {403}, number = {2-3}, pages = {347--372}, doi = {10.1016/j.tcs.2008.06.001}, ) @phdthesis(gim:phd, author = {St{\'e}phane Gimenez}, year = {2009}, title = {{Programming, Computation and their Analysis using Nets from Linear Logic}}, type = {Theses}, school = {{Universit{\'e} Paris Diderot}}, url = {https://tel.archives-ouvertes.fr/tel-00629013}, ) @inproceedings(Gimenez11, author = {St{\'{e}}phane Gimenez}, year = {2011}, title = {Realizability Proof for Normalization of Full Differential Linear Logic}, booktitle = {Typed Lambda Calculi and Applications - 10th International Conference, {TLCA} 2011}, series = {Lecture Notes in Computer Science}, volume = {6690}, publisher = {Springer}, pages = {107--122}, doi = {10.1007/978-3-642-21691-6\_11}, ) @article(Girard87, author = {Jean{-}Yves Girard}, year = {1987}, title = {Linear Logic}, journal = {Theor. Comput. Sci.}, volume = {50}, pages = {1--102}, doi = {10.1016/0304-3975(87)90045-4}, ) @article(Girard01, author = {Jean{-}Yves Girard}, year = {2001}, title = {Locus Solum: From the rules of logic to the logic of rules}, journal = {Mathematical Structures in Computer Science}, volume = {11}, number = {3}, pages = {301--506}, doi = {10.1017/S096012950100336X}, ) @inproceedings(GuerrieriPellissierTortora16, author = {Giulio Guerrieri and Luc Pellissier and Lorenzo Tortora de Falco}, year = {2016}, title = {Computing Connected Proof(-Structure)s From Their Taylor Expansion}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction, {FSCD} 2016}, series = {LIPIcs}, volume = {52}, publisher = {Schloss Dagstuhl}, pages = {20:1--20:18}, doi = {10.4230/LIPIcs.FSCD.2016.20}, ) @inproceedings(GuerrieriPellissierTortora19, author = {Giulio Guerrieri and Luc Pellissier and Lorenzo Tortora de Falco}, year = {2019}, title = {Proof-Net as Graph, Taylor Expansion as Pullback}, booktitle = {Logic, Language, Information, and Computation - 26th International Workshop, WoLLIC 2019}, series = {Lecture Notes in Computer Science}, volume = {11541}, publisher = {Springer}, pages = {282--300}, doi = {10.1007/978-3-662-59533-6\_18}, ) @inproceedings(GuerrieriPellissierTortora20, author = {Giulio Guerrieri and Luc Pellissier and Lorenzo Tortora de Falco}, year = {2020}, title = {Glueability of Resource Proof-Structures: Inverting the Taylor Expansion}, booktitle = {28th {EACSL} Annual Conference on Computer Science Logic, {CSL} 2020}, series = {LIPIcs}, volume = {152}, publisher = {Schloss Dagstuhl}, pages = {24:1--24:18}, doi = {10.4230/LIPIcs.CSL.2020.24}, ) @techreport(guglielmi1999calculus, author = {Alessio Guglielmi}, year = {1999}, title = {A Calculus of Order and Interaction}, type = {Technical Report}, number = {WV-1999-04}, institution = {Department of Computer Science, Dresden University of Technology}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.6332}, ) @article(gug:SIS, author = {Alessio Guglielmi}, year = {2007}, title = {A System of Interaction and Structure}, journal = {{ACM} Trans. Comput. Log.}, volume = {8}, number = {1}, pages = {1--64}, doi = {10.1145/1182613.1182614}, ) @inproceedings(gug:gun:par:2010, author = {Alessio Guglielmi and Tom Gundersen and Michel Parigot}, year = {2010}, title = {{A Proof Calculus Which Reduces Syntactic Bureaucracy}}, booktitle = {Proceedings of the 21st International Conference on Rewriting Techniques and Applications, {RTA} 2010}, series = {LIPIcs}, volume = {6}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, pages = {135--150}, doi = {10.4230/LIPIcs.RTA.2010.135}, ) @inproceedings(gug:str:01, author = {Alessio Guglielmi and Stra{\ss}burger, Lutz}, year = {2001}, title = {Non-commutativity and {MELL} in the Calculus of Structures}, editor = {Laurent Fribourg}, booktitle = {Computer Science Logic, 15th International Workshop, {CSL} 2001}, series = {Lecture Notes in Computer Science}, volume = {2142}, publisher = {Springer}, pages = {54--68}, doi = {10.1007/3-540-44802-0\_5}, ) @inproceedings(gug:str:02, author = {Alessio Guglielmi and Stra{\ss}burger, Lutz}, year = {2002}, title = {A Non-commutative Extension of {MELL}}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, {LPAR} 2002}, series = {Lecture Notes in Computer Science}, volume = {2514}, publisher = {Springer}, pages = {231--246}, doi = {10.1007/3-540-36078-6\_16}, ) @article(horne2019morgan, author = {Ross Horne and Alwen Tiu and Bogdan Aman and Gabriel Ciobanu}, year = {2019}, title = {De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic}, journal = {ACM Transactions on Computational Logic (TOCL)}, volume = {20}, number = {4}, pages = {22:1--22:44}, doi = {10.1145/3325821}, ) @inproceedings(Lafont90, author = {Yves Lafont}, year = {1990}, title = {Interaction Nets}, booktitle = {Seventeenth Annual {ACM} Symposium on Principles of Programming Languages, {POPL} 1990}, publisher = {{ACM} Press}, pages = {95--108}, doi = {10.1145/96709.96718}, ) @article(Mazza18, author = {Damiano Mazza}, year = {2018}, title = {The true concurrency of differential interaction nets}, journal = {Math. Struct. Comput. Sci.}, volume = {28}, number = {7}, pages = {1097--1125}, doi = {10.1017/S0960129516000402}, ) @inproceedings(MazzaPagani07, author = {Damiano Mazza and Michele Pagani}, year = {2007}, title = {The Separation Theorem for Differential Interaction Nets}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, {LPAR} 2007}, series = {Lecture Notes in Computer Science}, volume = {4790}, publisher = {Springer}, pages = {393--407}, doi = {10.1007/978-3-540-75560-9\_29}, ) @book(milner:pi, author = {Robin Milner}, year = {1999}, title = {Communicating and Mobile Systems: the Pi Calculus}, publisher = {Cambridge University Press}, address = {New York, NY, USA}, ) @inproceedings(Pagani09, author = {Michele Pagani}, year = {2009}, title = {The Cut-Elimination Theorem for Differential Nets with Promotion}, booktitle = {Typed Lambda Calculi and Applications, 9th International Conference, {TLCA} 2009}, series = {Lecture Notes in Computer Science}, volume = {5608}, publisher = {Springer}, pages = {219--233}, doi = {10.1007/978-3-642-02273-9\_17}, ) @inproceedings(PaganiTasson09, author = {Michele Pagani and Christine Tasson}, year = {2009}, title = {The Inverse Taylor Expansion Problem in Linear Logic}, booktitle = {Proceedings of the 24th Annual {IEEE} Symposium on Logic in Computer Science, {LICS} 2009, 11-14 August 2009, Los Angeles, CA, {USA}}, publisher = {{IEEE} Computer Society}, pages = {222--231}, doi = {10.1109/LICS.2009.35}, ) @article(PaganiTranquilli17, author = {Michele Pagani and Paolo Tranquilli}, year = {2017}, title = {The conservation theorem for differential nets}, journal = {Mathematical Structures in Computer Science}, volume = {27}, number = {6}, pages = {939--992}, doi = {10.1017/S0960129515000456}, ) @phdthesis(ralph:phd, author = {Benjamin Ralph}, year = {2019}, title = {Modular Normalisation of Classical Proofs}, school = {University of Bath}, url = {https://researchportal.bath.ac.uk/files/189585932/thesis_ralph_final.pdf}, ) @phdthesis(str:phd, author = {Stra{\ss}burger, Lutz}, year = {2003}, title = {Linear Logic and Noncommutativity in the Calculus of Structures}, school = {Technische Universit\"at Dresden}, ) @article(str:MELLinCoS, author = {Stra\IeC{\ss}burger, Lutz}, year = {2003}, title = {MELL in the calculus of structures}, journal = {Theoretical Computer Science}, volume = {309}, number = {1}, pages = {213 -- 285}, doi = {10.1016/S0304-3975(03)00240-8}, ) @inproceedings(Tranquilli09, author = {Paolo Tranquilli}, year = {2009}, title = {Confluence of Pure Differential Nets with Promotion}, booktitle = {Computer Science Logic, 23rd international Workshop, {CSL} 2009, 18th Annual Conference of the EACSLS}, series = {Lecture Notes in Computer Science}, volume = {5771}, publisher = {Springer}, pages = {500--514}, doi = {10.1007/978-3-642-04027-6\_36}, ) @article(Tranquilli11, author = {Paolo Tranquilli}, year = {2011}, title = {Intuitionistic differential nets and lambda-calculus}, journal = {Theor. Comput. Sci.}, volume = {412}, number = {20}, pages = {1979--1997}, doi = {10.1016/j.tcs.2010.12.022}, ) @phdthesis(tubella:phd, author = {Andrea Aler Tubella}, year = {2017}, title = {A study of normalisation through subatomic logic}, school = {University of Bath}, url = {https://researchportal.bath.ac.uk/files/187926411/thesis.pdf}, ) @article(TubellaGuglielmi18, author = {Andrea Aler Tubella and Alessio Guglielmi}, year = {2018}, title = {Subatomic Proof Systems: Splittable Systems}, journal = {{ACM} Trans. Comput. Log.}, volume = {19}, number = {1}, pages = {5:1--5:33}, doi = {10.1145/3173544}, ) @unpublished(tub:str:esslli19, author = {Andrea Aler Tubella and Stra{\ss}burger, Lutz}, year = {2019}, title = {{Introduction to Deep Inference}}, url = {https://hal.inria.fr/hal-02390267}, note = {Lecture}, )