[TYPES/announce] Normalisation Control in Deep Inference Via Atomic Flows

[Alessio Guglielmi]

Dear colleagues,

Tom Gundersen and I would like to advertise a paper on a new proof 
normalisation method, which might be of interest to the types 
community: <http://cs.bath.ac.uk/ag/p/NormContrDIAtFl.pdf>. Comments 
are very welcome.

Cheers,

-Alessio Guglielmi


Normalisation Control in Deep Inference Via Atomic Flows

We introduce diagrams, called 'atomic flows', that forget much of the 
syntactic structure of derivations and only retain causal relations 
between atoms. Using atomic flows on propositional logic, we can 
design and control several normalisation procedures. In particular, 
we can obtain cut elimination as a special case of more general 
normal forms. This technique only relies on substituting derivations 
in the place of atoms, similarly to natural deduction, and not on 
permuting inference steps, as in the sequent calculus. Because they 
abstract away from most syntactic details, atomic flows allow for 
very simple control of normalisation procedures, which would be 
otherwise cumbersome in the bare syntax. We operate in deep 
inference, a very general methodology, where normalisation is more 
difficult to control than in other syntactic paradigms.

Deep inference web page: <http://alessio.guglielmi.name/res/cos>