Publications

@article{bfs2020,
    author = {Brünnler, Kai and Flumini, Dandolo and Studer, Thomas},
    title = "{A logic of blockchain updates}",
    journal = {Journal of Logic and Computation},
    volume = {30},
    number = {8},
    pages = {1469-1485},
    year = {2020},
    month = {09},
    issn = {0955-792X},
    doi = {10.1093/logcom/exaa045},
    url = {https://doi.org/10.1093/logcom/exaa045},
    eprint = {https://academic.oup.com/logcom/article-pdf/30/8/1469/34673218/exaa045.pdf},
}

@article {bs12,
	title = {Syntactic cut-elimination for a fragment of the modal mu-calculus},
	journal = {Annals of Pure and Applied Logic},
	volume = {163},
	number = {12},
	year = {2012},
	pages = {1838-1853},
	url = {http://www.iam.unibe.ch/ltgpub/2012/bs12.pdf},
	author = {Kai Br{\"u}nnler and Thomas Studer}
}

@article{Br09,
  title = "Deep Sequent Systems for Modal Logic",
  journal = "Archive for Mathematical Logic",
  volume = "48",
  number = "6",
  pages = "551--577",
  year = "2009",
  author = "Kai Br{\"u}nnler",
}

@article{BrSt09,
  title = "Syntactic cut-elimination for common knowledge",
  journal = "Annals of Pure and Applied Logic",
  volume = "160",
  number = "1",
  pages = "82 - 95",
  year = "2009",
  issn = "0168-0072",
  doi = "DOI: 10.1016/j.apal.2009.01.014",
  author = "Kai Br{\"u}nnler and Thomas Studer",
}

@article{BrLa08,
  title = "Cut-free sequent systems for temporal logic",
  journal = "Journal of Logic and Algebraic Programming",
  volume = "76",
  number = "2",
  pages = "216 - 225",
  year = "2008",
  issn = "1567-8326",
  doi = "DOI: 10.1016/j.jlap.2008.02.004",
  author = "Kai Br{\"u}nnler and Martin Lange",
}

@article{BPS08,
  author = {Br{\"u}nnler, Kai and Probst, Dieter and Studer, Thomas},
  title = {On contraction and the modal fragment},
  year = {2008},
  journal = {Mathematical Logic Quarterly},
  volume = {54},
  number = {4},
  pages = {345{--}349},
}

@article{Bru06, 
  author = {Kai {Br\"unnler}}, 
  title = {Cut Elimination inside a Deep Inference System for Classical Predicate Logic}, 
  year = 2006, 
  number = 1, 
  journal = {Studia Logica}, 
  volume = 82, 
  pages = "51--71"
}

@article{BruLCL06,
  author = {Kai {Br\"unnler}},
  title = {Locality for Classical Logic},
  journal = {Notre Dame Journal of Formal Logic},
  year = {2006},
  volume = {47},
  pages = {557--580}
}

@article{BruRC03, 
  author = {Kai {Br\"unnler}}, 
  title = {Two Restrictions on Contraction}, 
  year = 2003, 
  number = 5, 
  journal = {Logic Journal of the IGPL}, 
  volume = 11, 
  pages = "525--529"
}

@InProceedings{boss_et_al:OASIcs:2020:13421,
  author =	{Ramon Boss and Kai Br{\"u}nnler and Anna Doukmak},
  title =	{{Towards Verifying the Bitcoin-S Library (Short Paper)}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{8:1--8:9},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bruno Bernardo and Diego Marmsoler},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13421},
  URN =		{urn:nbn:de:0030-drops-134212},
  doi =		{10.4230/OASIcs.FMBC.2020.8},
  annote =	{Keywords: Bitcoin, Scala, Bitcoin-S, Stainless}
}

@inproceedings{DBLP:conf/lfcs/BrunnlerFS18,
  author    = {Kai Br{\"{u}}nnler and
               Dandolo Flumini and
               Thomas Studer},
  title     = {A Logic of Blockchain Updates},
  booktitle = {Logical Foundations of Computer Science - International Symposium,
               {LFCS} 2018, Deerfield Beach, FL, USA, January 8-11, 2018, Proceedings},
  pages     = {107--119},
  year      = {2018},
  crossref  = {DBLP:conf/lfcs/2018},
  url       = {https://doi.org/10.1007/978-3-319-72056-2\_7},
  doi       = {10.1007/978-3-319-72056-2\_7},
  timestamp = {Sun, 31 Dec 2017 12:03:46 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/lfcs/BrunnlerFS18},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@incollection{Bru10,
   author = {Br{\"u}nnler, Kai},
   title = {How to Universally Close the Existential Rule},
   booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning},
   series = {Lecture Notes in Computer Science},
   editor = {Ferm{\"u}ller, Christian and Voronkov, Andrei},
   publisher = {Springer},
   pages = {172-186},
   volume = {6397},
   url = {http://dx.doi.org/10.1007/978-3-642-16242-8_13},
   year = {2010},
   note = {\url{http://www.iam.unibe.ch/~kai/Papers/2010hucer.pdf}},
}

@incollection{BGK10,
  author = {Kai Br{\"u}nnler and Remo Goetschi and Roman Kuznets},
  title = {A Syntactic Realization Theorem for Justification Logics},
  booktitle = {Advances in Modal Logic, Volume 8},
  publisher = {College Publications},
  year = {2010},
  editor = {Lev Beklemishev and Valentin Goranko and Valentin Shehtman},
  pages = {39--58},
  note = {\url{http://www.iam.unibe.ch/~kai/Papers/2010srtjl.pdf}},
}

@inproceedings{BrStr09,
  Author = {Br{\"u}nnler, Kai and Stra{\ss}burger, Lutz},
  Booktitle = {Tableaux 2009},
  Editor = {Giese, Martin and Waaler, Arild},
  Publisher = {Springer-Verlag},
  Series = {Lecture Notes in Computer Science},
  Title = {Modular Sequent Systems for Modal Logic},
  Volume = {5607},
  Year = {2009},
  Pages = {152--166}
}

@inproceedings{BrMc08,
  Author = {Br{\"u}nnler, Kai and McKinley, Richard},
  Booktitle = {LPAR 2008},
  Editor = {Cervesato, I. and Veith, H. and Voronkov, A.},
  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}
}

@article{BruStu07,
  author = {Kai Br{\"u}nnler and Thomas Studer},
  title = "Syntactic Cut-elimination for Common Knowledge",
  journal = "Electronic Notes in Theoretical Computer Science",
  volume = "231",
  number = "",
  pages = "227 - 240",
  year = "2009",
  note = "Proceedings of the 5th Workshop on Methods for Modalities (M4M5 2007)",
}

@CONFERENCE{Bru06ds,
  author = {Br{\"u}nnler, Kai},
  title = {Deep Sequent Systems for Modal Logic},
  booktitle = {Advances in Modal Logic},
  year = {2006},
  editor = {Guido Governatori and Ian Hodkinson and Yde Venema},
  volume = {6},
  pages = {107--119},
  publisher = {College Publications}
}

@INPROCEEDINGS{Bru06nf,
  author = {Br{\"u}nnler, Kai},
  title = {Deep inference and its normal form of derivations},
  booktitle = {Logical Approaches to Computational Barriers, Second Conference on
	Computability in Europe},
  year = {2006},
  editor = {Arnold Beckmann, Ulrich Berger, Benedikt L{\"o}we, John V Tucker},
  volume = {3988},
  series = {Lecture Notes in Computer Science},
  pages = {65--74},
  publisher = {Springer-Verlag}
}

@INCOLLECTION{BruGugFin,
  author = {Br\"unnler, Kai and Guglielmi, Alessio},
  title = {A First Order System with Finite Choice of Premises},
  booktitle = {First-Order Logic Revisited},
  publisher = {Logos Verlag},
  year = {2004},
  editor = {Vincent Hendricks and Fabian Neuhaus and Stig Andur Pedersen and
	Uwe Scheffler and Heinrich Wansing},
  pages = {59--74},
  city = {Berlin}
}

@INPROCEEDINGS{BruACECL,
  author = {Br\"unnler, Kai},
  title = {Atomic Cut Elimination for Classical Logic},
  booktitle = {CSL 2003},
  year = {2003},
  editor = {M. Baaz and J. A. Makowsky},
  volume = {2803},
  series = {Lecture Notes in Computer Science},
  pages = {86--97},
  publisher = {Springer-Verlag}
}

@INPROCEEDINGS{BruTiu01,
  author = {Br\"unnler, Kai and Tiu, Alwen Fernanto},
  title = {A Local System for Classical Logic},
  booktitle = {LPAR 2001},
  year = {2001},
  editor = {R. Nieuwenhuis and A. Voronkov},
  volume = {2250},
  series = {Lecture Notes in Artificial Intelligence},
  pages = {347--361},
  publisher = {Springer-Verlag}
}

@INPROCEEDINGS{BruLen05,
  author = {Br\"unnler, Kai and Lengrand, St\'ephane},
  title = {On Two Forms of Bureaucracy in Derivations},
  booktitle = {Structures and Deduction},
  year = {2005},
  editor = {Paola Bruscoli and {Fran{\c c}ois} Lamarche and Charles Stewart},
  pages = {69--80},
  publisher = {Technische Universit\"at Dresden}
}

@misc{BruHabil,
   author =  {Kai Br\"unnler},
   title =   {Nested Sequents},
   school =  {Universit\"at Bern},
   year =    2010,
   url = {http://arxiv.org/abs/1004.1845v1},
   }

@PHDTHESIS{BruTh,
  author = {Br\"unnler, Kai},
  title = {Deep Inference and Symmetry in Classical Proofs},
  school = {Technische Universit{\"a}t Dresden},
  year = {2003},
}

@MASTERSTHESIS{BruMS,
   author =  {Kai Br{\"u}nnler},
   title =   {Mechanizing Coinduction with Maude},
   school =  {Technische Universit{\"a}t Dresden},
   year =    2000
}