Anupam Das

I have a new blog post with Ian Shillito and Jim de Groot: prooftheory.blog/2025/10/03/dia… . In it we complete the classification of intuitionistic modal logics by their Diamond-free parts. It's been a whirlwind story, involving both automated and interactive theorem proving!

Dale Miller has shared a memoriam and some enlightening personal reflections about the late Peter Andrews on the Proof Theory Blog: * prooftheory.blog/2025/06/17/in-… * prooftheory.blog/2025/06/17/per…

I have a new blog post comparing exponentials with their fixed point encodings in linear logic on The Proof Theory Blog: prooftheory.blog/2024/06/27/exp… . Any comments are welcome!

Timo Lang has written a cool post on the Proof Theory Blog about the conservativity of extending constructive modal logics by a normal diamond. He has a one line proof! prooftheory.blog/2024/03/20/a-n…

@FellowHominid I think something like this is possible (and if so folklore). It is similar to adding the general 'mix' rule, which I believe renders cut-elimination confluent in LK (?). Would make for a good blog post! ;)

@ADasAcademic (2/2) another way to think about this maybe: given classical logic we can polarise propositions which correspond to choosing different evaluation orders. I'd like to say that the computational content of a classical proof is the formal sum of all the different possible ...

Ever wondered about why cut-elimination in the sequent calculus is problematic from proofs-as-programs point of view? Boris Eng and Farzad Jaffarahmani investigate (non-)confluence of cut-elimination in the latest post on the Proof Theory Blog: prooftheory.blog/2021/09/23/con… .

What happens when intuitionism and modalities interact? Sonia Marin and I discuss the state of the art in a new blog post: prooftheory.blog/2022/08/19/bro…

Dale Miller has written an excellent post on the Proof Theory Blog on the decomposition of intuitionistic logic via linear logic: prooftheory.blog/2022/07/06/lk-…. Dale argues that Gentzen's calculus LJ naturally induces Girard's linear logic.

I have (another) postdoc opening in my group at Birmingham: jobs.ac.uk/job/CPP274/pos… . Please let interested students/postdocs to get in touch with me informally first. The deadline is 29 May.

I have a postdoctoral position opening in my group in Birmingham: jobs.ac.uk/job/CLO630/res… . Please encourage your students/postdocs to consider applying! I am available for informal enquiries (preferably before Christmas).

I've been back on the Type Theory For All podcast with @p_droabreu0, this time debating @taooftypes on a hot topic: constructivism vs classicism. Check it out! typetheoryforall.com

Daniel Murfet and I have a joint Birmingham-Melbourne PhD opportunity available, on the proof theory and algebra of fixed points: findaphd.com/phds/project/p… . Please advertise this to your students!

I recently sat down with @p_droabreu0 for a discussion about proof theory and foundations on his podcast, Type Theory for All. You can find it here: typetheoryforall.com

The Tableaux 2021 deadline has been extended to 26 April / 30 April. Please consider submitting! tableaux2021.org

Thank you to all those who attended/organised the Midlands Graduate School last week. It was probably the best virtual event I have experienced during this awful pandemic. FYI, I will keep my Proof Theory course page available for reference: anupamdas.com/mgs21 .

@ArneMeier @SaskiaHeijltjes Hi, sorry for that, it should be back up now. We were hit with DNS issues at the worst time! Let me know if you have problems again.

Today I'm pleased to announce the launch of the Proof Theory Blog: prooftheory.blog , a new collaborative community project for discussing ideas, works-in-progress and folklore relating to Proof Theory. Please read, comment and contribute!

I have funding for 2 postdocs in Proof Theory at Birmingham: jobs.ac.uk/job/CAD990/res… . Please get in touch if you are interested in applying!

I am delighted to announce that I have won a UKRI Future Leaders Fellowship worth £1.4million! ukri.org/news/new-round… More details, including PhD/postdoc offers, will be available on my webpage soon.

I am visiting the University of California, San Diego from 28 Jan - 8 Mar. math.ucsd.edu