For a new seminar of the proofs and algorithms pole of LIX, we are happy to welcome Paolo Pistone for a talk entitled On Equivalence and Similarity of Polymorphic Proofs and Programs.

Link to the online conference

Abstract: Under the proofs-as-programs paradigm, the problem of program equivalence, that is, of understanding whether two programs compute the same function, can be related to the problem of equivalence proof, that is of understanding whether two formal derivations represent, in some sense, the same proof. In this talk I will discuss some methods to capture program/proof equivalence in System F, the paradigmatic language for parametric polymorphism, through the definition of an invariant, for each type, called the characteristic, This invariant provides a means to know whether, in the proofs of a given formula, propositional quantification (i.e. polymorphism) is eliminable via parametricity, yielding a way to test equivalence in a finite way. Moreover, I will sketch how parametricity and related methods for equivalence can be lifted to a more quantitative setting (as those arising from probabilistic or approximate computation) in which the vital property to understand is whether two programs, albeit non-equivalent, behave in a sufficiently similar way, so that replacing the one by the other cannot alter the results of computation too much.

The list of next seminars can be found at: https://smimram.gitlabpages.inria.fr/proofs-algorithms/seminar/

The calendar of seminars can be found at: https://smimram.gitlabpages.inria.fr/proofs-algorithms/seminar/calendar.ics