Workshop on Efficient and Natural Proof Systems: Call for participation. 14-16 December, Bath.
Anupam Das <[email protected]> Fri, 13 Nov 2015 01:29:06 +0100
| Newsgroups | gmane.science.mathematics.frogs |
|---|---|
| Message-ID | <[email protected]> |
This is a multi-part message in MIME format. --------------010004080204040703090805 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit CALL FOR PARTICIPATION Workshop on EFFICIENT AND NATURAL PROOF SYSTEMS University of Bath 14-16 December, 2015 <http://www.cs.bath.ac.uk/ag/ENPS/wenps2015.html> The Mathematical Foundations group at the Department of Computer Science, University of Bath, will host a 2.5-day workshop on structural proof theory, starting in the afternoon of 14 December. The workshop will focus on the various aspects of structural proof theory, including but not limited to the following topics: - deep inference proof theory - algebraic, combinatorial and geometric representations of proofs - proof compression - normalisation of proofs - proof checking - proof search - complexity of proofs - computational interpretations of proofs PARTICIPATION There is no fee or formal registration for the workshop and anyone is welcome to attend. However we ask that anyone who intends to attend informs us by *20 November* so that we may accordingly plan coffee breaks and social activities. All enquiries should be made to <<mailto:wenps2015-bC77Qfv0vuxrovVCs/[email protected]>mailto:wenps2015-bC77Qfv0vuxrovVCs/[email protected]>. SPEAKERS Andrea Aler Tubella (Bath). A generalised cut-elimination procedure through subatomic logic. Marc Bagnol (Ottawa). Complexity of MALL proofnets and binary decision trees. Arnold Beckmann (Swansea). TBA. Stefano Berardi (Turin). A confluence-free proof of SN for the simply typed lambda-calculus. Taus Brock-Nannestad (Inria Saclay). Reconciling Two Notions of Cut Elimination. Roy Dyckhoff (St Andrews). Coherentisation of first-order logic. Alessio Guglielmi (Bath). TBA. Tom Gundersen (Red Hat). TBA. Fanny He (Bath). Towards an atomic lambda-mu-calculus. Björn Lellmann (Vienna). Linear Nested Sequents. Sonia Marin (Inria Saclay). Focused and Synthetic Nested Sequents. Dale Miller (Inria Saclay). Designing an assembly language for computational logic. Georg Moser (Innsbruck). TBA. Michel Parigot (PPS, Paris). TBA. Thomas Powell (Innsbruck). Variations on Learning: Relating the epsilon calculus to proof interpretations. Benjamin Ralph (Bath). A Natural Cut Elimination Procedure for Classical First-Order Logic. Simona Ronchi Della Rocca (Turin). Intersection Types and Implicit Computational Complexity. Luca Roversi (Turin). A Class of Recursive Reversible Functions. Marco Volpe (Inria Saclay). Focused proof systems for modal logic. COURSE ON DEEP INFERENCE *Change of time*: 14 December 11:00 to 13:00. (Due to the high quality and number of contributions received by the committee, we have decided to replace the previously advertised course on deep inference by an abridged version on the morning preceding the workshop.) Deep inference is a modern proof theory offering a better understanding of proofs and extending the range of applications of traditional Gentzen proof theory. This course will offer a brief introduction to deep inference. CHILDCARE The Department of Computer Science and the University of Bath are committed to a supportive and inclusive working environment. Childcare will be provided to workshop participants and their children if required. If you need this service, please contact us at <mailto:wenps2015-bC77Qfv0vuxrovVCs/[email protected]> by 20 November. ACCESSIBILITY If you have requests concerning accessibility or dietary requirements, please contact us at <mailto:wenps2015-bC77Qfv0vuxrovVCs/[email protected]> and we will do all we can to assist. ORGANISING AND PROGRAMME COMMITTEE Paola Bruscoli (Bath) Anupam Das (ENS Lyon) Willem Heijltjes (Bath) Lutz Straßburger (Inria) FUNDING EPSRC Project EP/K018868/1 'Efficient and Natural Proof Systems' <http://www.cs.bath.ac.uk/ag/ENPS/>. --------------010004080204040703090805 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 8bit <html> <head> <meta http-equiv="content-type" content="text/html; charset=utf-8"> </head> <body text="#000000" bgcolor="#FFFFFF"> <meta charset="utf-8"> <tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">CALL FOR PARTICIPATION </span></tt><tt><br> </tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Workshop on EFFICIENT AND NATURAL PROOF SYSTEMS</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">University of Bath</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">14-16 December, 2015</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;"><a class="moz-txt-link-rfc2396E" href="http://www.cs.bath.ac.uk/ag/ENPS/wenps2015.html"><http://www.cs.bath.ac.uk/ag/ENPS/wenps2015.html></a></span></tt><tt><br> </tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">The Mathematical Foundations group at the Department of Computer Science, University of Bath, will host a 2.5-day workshop on structural proof theory, starting in the afternoon of 14 December.</span></tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">The workshop will focus on the various aspects of structural proof theory, including but not limited to the following topics:</span></tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">- deep inference proof theory</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">- algebraic, combinatorial and geometric representations of proofs</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">- proof compression</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">- normalisation of proofs</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">- proof checking</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">- proof search</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">- complexity of proofs</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">- computational interpretations of proofs</span></tt><tt><br> </tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">PARTICIPATION</span></tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">There is no fee or formal registration for the workshop and anyone is welcome to attend. However we ask that anyone who intends to attend informs us by *20 November* so that we may accordingly plan coffee breaks and social activities.</span></tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">All enquiries should be made to <</span></tt><tt><a href="mailto:wenps2015-bC77Qfv0vuxrovVCs/[email protected]" style="text-decoration:none;"><span style="font-size: 13.3333px; color: rgb(17, 85, 204); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: underline; vertical-align: baseline;"></span></a><a class="moz-txt-link-freetext" href="mailto:wenps2015-bC77Qfv0vuxrovVCs/[email protected]"><a class="moz-txt-link-freetext" href="mailto:wenps2015-bC77Qfv0vuxrovVCs/[email protected]">mailto:wenps2015-bC77Qfv0vuxrovVCs/[email protected]</a></a></tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">>.</span></tt><tt><br> </tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">SPEAKERS </span></tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Andrea Aler Tubella (Bath). A generalised cut-elimination procedure through subatomic logic.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Marc Bagnol (Ottawa). Complexity of MALL proofnets and binary decision trees.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Arnold Beckmann (Swansea). TBA.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Stefano Berardi (Turin). A confluence-free proof of SN for the simply typed lambda-calculus.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Taus Brock-Nannestad (Inria Saclay). Reconciling Two Notions of Cut Elimination.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Roy Dyckhoff (St Andrews). Coherentisation of first-order logic.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Alessio Guglielmi (Bath). TBA.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Tom Gundersen (Red Hat). TBA.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Fanny He (Bath). Towards an atomic lambda-mu-calculus.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Björn Lellmann (Vienna). Linear Nested Sequents.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Sonia Marin (Inria Saclay). Focused and Synthetic Nested Sequents.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Dale Miller (Inria Saclay). Designing an assembly language for computational logic.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Georg Moser (Innsbruck). TBA.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Michel Parigot (PPS, Paris). TBA.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Thomas Powell (Innsbruck). Variations on Learning: Relating the epsilon calculus to proof interpretations.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Benjamin Ralph (Bath). A Natural Cut Elimination Procedure for Classical First-Order Logic.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Simona Ronchi Della Rocca (Turin). Intersection Types and Implicit Computational Complexity.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Luca Roversi (Turin). A Class of Recursive Reversible Functions.</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Marco Volpe (Inria Saclay). Focused proof systems for modal logic.</span></tt><tt><br> </tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">COURSE ON DEEP INFERENCE</span></tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">*Change of time*: 14 December 11:00 to 13:00.</span></tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">(Due to the high quality and number of contributions received by the committee, we have decided to replace the previously advertised course on deep inference by an abridged version on the morning preceding the workshop.)</span></tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Deep inference is a modern proof theory offering a better understanding of proofs and extending the range of applications of traditional Gentzen proof theory. This course will offer a brief introduction to deep inference.</span></tt><tt><br> </tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">CHILDCARE</span></tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">The Department of Computer Science and the University of Bath are committed to a supportive and inclusive working environment. Childcare will be provided to workshop participants and their children if required. If you need this service, please contact us at <a class="moz-txt-link-rfc2396E" href="mailto:wenps2015-bC77Qfv0vuxrovVCs/[email protected]"><a class="moz-txt-link-rfc2396E" href="mailto:wenps2015-bC77Qfv0vuxrovVCs/[email protected]"><mailto:wenps2015-bC77Qfv0vuxrovVCs/[email protected]></a></a> by 20 November.</span></tt><tt><br> </tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">ACCESSIBILITY</span></tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">If you have requests concerning accessibility or dietary requirements, please contact us at <a class="moz-txt-link-rfc2396E" href="mailto:wenps2015-bC77Qfv0vuxrovVCs/[email protected]"><a class="moz-txt-link-rfc2396E" href="mailto:wenps2015-bC77Qfv0vuxrovVCs/[email protected]"><mailto:wenps2015-bC77Qfv0vuxrovVCs/[email protected]></a></a> and we will do all we can to assist.</span></tt><tt><br> </tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">ORGANISING AND PROGRAMME COMMITTEE</span></tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Paola Bruscoli (Bath)</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Anupam Das (ENS Lyon)</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Willem Heijltjes (Bath)</span></tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">Lutz Straßburger (Inria)</span></tt><tt><br> </tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">FUNDING</span></tt><tt><br> </tt><tt><br> </tt><tt><span style="font-size: 13.3333px; color: rgb(0, 0, 0); background-color: transparent; font-weight: 400; font-style: normal; font-variant: normal; text-decoration: none; vertical-align: baseline;">EPSRC Project EP/K018868/1 'Efficient and Natural Proof Systems' <a class="moz-txt-link-rfc2396E" href="http://www.cs.bath.ac.uk/ag/ENPS/"><http://www.cs.bath.ac.uk/ag/ENPS/></a>.</span></tt> </body> </html> --------------010004080204040703090805--