Vivek Nigam,

Vivek Nigam
A Framework for Specifying and Reasoning about Proof Systems

In this talk, I will introduce an on-going project whose objective is to build a framework that can facilitate the design and development of proof systems. In the first part of the talk, I will show how one can specify a wide number of proof systems in the logical framework called SELLF, which is based on linear logic with subexponentials. Then I will present novel techniques to reason automatically about proof systems. In particular, I will demonstrate how one can check automatically two important properties of proof systems, namely, whether a proof system admits cut-elimination and which inference rules of the encoded proof system permute over other rules. If time permits, I might run a demo on the latter application.