Normalisation & Equivalence in Proof Theory & Type Theory

摘要: At the heart of connections between Proof Theory and Type Theory, Curry-Howard correspondence provides proof-terms with computational features equational theories, i.e. notions normalisation equivalence. This dissertation contributes to extend its framework in directions proof-theoretic formalisms (such as sequent calculus) that are appealing for logical purposes like proof-search, powerful systems beyond propositional logic such type classical (rather than intuitionistic) reasoning. Part I is entitled Proof-terms Intuitionistic Implicational Logic. Its contributions use rewriting techniques on natural deduction (lambda-calculus) calculus, investigate cut-elimination, call-by-name call-by-value semantics. In particular, it introduces proof-term calculi multiplicative depth-bounded calculus G4. The former gives rise a explicit substitutions, weakenings contractions refines lambda-calculus beta-reduction, preserves strong full notion composition substitutions. latter new insight cut-elimination II, Sequent Calculus develops theory Pure Calculi (PTSC), which equivalent (with respect provability normalisation) Systems but better suited connection proof-assistant tactics enumeration algorithms. III, Towards Classical Logic, presents some approaches theory. particular version System Fomega. Beyond theory, equivalence proofs becomes crucial and, based parallel Structures, we compute canonical representatives proofs.