This seminar has been rescheduled. Please note the non-standard day and time. Franco will be visiting from Thursday to Saturday, hosted by Adriana Compagnoni.

Abstract

The symmetric lambda-calculus is a natural deduction system for Peano Arithmetic that was developed in order to provide a basis for the programming-with-proofs paradigm in a classical logic setting. We shall present its main features, among which are Strong Normalization and "non-confluence". We develop in the system a formal proof for a formula that can be seen as a simple but meaningful program specification. The computational behaviour of the corresponding term can be roughly analysed by interpreting it as a (higher-order communicating) process formed by distinct subprocesses which co-operate in different ways, producing different results, according to the reduction strategy used. We also show how to restrict the system in order to get confluence without loosing its computational features. The restricted system enables us to argue for the expressive power of symmetric and non-deterministic calculi like ours.