Output details
11 - Computer Science and Informatics
University of Bath
A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae
<11>A large part of the 3-year, £550,000 EPSRC project `Efficient and Natural Proof Systems' in Bath (2013-16, PI: Guglielmi) aims to exploit the opportunities in proof compression brought to
light by this paper. Also, a newly formed collaboration with the University of Turin, via the 2-year, £12,000 Royal Society grant `Sharing and Sequentiality in Proof Systems with Locality' (2012-14, PIs: Guglielmi and Roversi), is in large part devoted to finding computational interpretations of proofs made possible by the sharing mechanism defined in this paper in order to obtain quasipolynomial normalisation.