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.