Por Paolo Pistone (Université Claude Bernard Lyon 1).
In the last few years there has been a rise of interest towards the study of canonical proof systems. In standard proof systems, like natural deduction or sequent calculus, it is often the case that distinct formal derivations may represent, intuitively or semantically, the same proof. Instead, in a canonical system distinct derivations should ideally correspond to intuitively or semantically distinct proofs. Beyond its relevance for proof theory and the identity of proofs problem (when are two proofs the same?), the study of such systems is important also from the viewpoint of programming language theory: via the Curry-Howard correspondence, semantically equivalent proofs correspond to equivalent programs, that is, to programs computing the same function; canonical proof systems provide then methods to understand program equivalence, a crucial ingredient of program verification. Different techniques to obtain canonical proof systems exist in the literature, from focused proof-search to linear logic proof nets and combinatorial proofs. Our project aims at studying canonical proofs for System F, that is, for propositional intuitionistic second order logic, by combining focused proof search with recent results on the categorical semantics of polymorphism. As System F provides the abstract architecture for many functional programming languages, our long term goal is thus to devise new methods to understand program equivalence for such languages.
Transmissão via Zoom (pw: 919 4789 5133).
