[FOM] Workshop on Efficient and Natural Proof Systems: Call for participation. 14-16 December, Bath.

[Anupam Das]

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 at easychair.org>mailto:wenps2015 at easychair.org>.


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 at easychair.org> by 20 November.


ACCESSIBILITY

If you have requests concerning accessibility or dietary requirements, 
please contact us at <mailto:wenps2015 at easychair.org> 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/>.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20151113/4fb46392/attachment-0001.html>