[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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>