Taus Brock-Nannestad

My research interests can mostly be grouped under the suitably general heading "formal methods", but more specifically include: structural proof theory, substructural logics, logical frameworks, and computer-verified proofs. My main interest these days is in the fine-grained structure of proofs in the sequent calculus, as seen through the lens of focusing. In addition to this, I am also interested in giving computational interpretations of focused calculi.

A secondary interest of mine is oriented towards improving the state of the art in finding ways of disproving theorems, especially in non-classical logics.

• Taus Brock-Nannestad, Danko Ilik. An Intuitionistic Formula Hierarchy Based on High-School Identities. Submitted. (arXiv)
• Taus Brock-Nannestad. Space-efficient Planar Acyclicity Constraints — A Declarative Pearl International Symposium on Functional and Logic Programming (FLOPS-13, March 2016). (PDF)
• Taus Brock-Nannestad, Kaustuv Chaudhuri. Disproving Using the Inverse Method by Iterated Refinement of Finite Approximations. Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-24, September 2015). (PDF)
  See the associated theorem prover, Mætning.
• Taus Brock-Nannestad, Nicolas Guenot, Daniel Gustafsson. Computation in Focused Intuitionistic Logic. Principles and Practice of Declarative Programming (PPDP 17, July 2015) (PDF)
• Taus Brock-Nannestad, Nicolas Guenot. Focused Linear Logic and the $λ$-calculus. Mathematical Foundations of Programming Semantics (MFPS XXXI, June 2015). (PDF)
• Taus Brock-Nannestad, Nicolas Guenot. Cut Elimination in Multifocused Linear Logic. International Workshop on Linearity (3rd LINEARITY, July 2014). (PDF)
• Taus Brock-Nannestad, Nicolas Guenot, Agata Murawska, Carsten Schürmann. Hybrid Extensions in a Logical Framework. International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (9th LFMTP, July 2014). (PDF)
• Taus Brock-Nannestad, Carsten Schürmann. Truthful Monadic Abstractions. International Joint Conference on Automated Reasoning (6th IJCAR, June 2012). (PDF)
• Taus Brock-Nannestad, Carsten Schürmann. Focused Natural Deduction. International Conference on Logic for Programming, Artificial Intelligence and Reasoning (17th LPAR, October 2010). (PDF)

• I am currently a post.doc. in Dale Miller's Parsifal team, working on the ProofCert project.
• In September 2014, I defended my dissertation and obtained the degree of Ph.d.
• From September 2009 through April 2014 I was enrolled and employed as a Master/Ph.d. student at the IT University of Copenhagen, supervised by Carsten Schürmann.
• I completed my undergraduate studies in the Mathematics department at Copenhagen University, obtaining a BSc in Mathematics.

My CV (updated September 2015) may be found here: CV.