Séminaire 2020-21 | Logique, Mathématiques, Informatique, Raisonnement

Coordination scientifique : Jean-Baptiste Joinet, Simone Martini, Wendy Hammache  et Yannis Hausberg
 

Programme du séminaire :
 

• Séance 1
  Jeudi 8 octobre de 18h à 20h
  Salle CH-314, 18 rue Chevreul - 69007 Lyon
  
  "The calculus of higher-level rules in modern dress (Joint work with Luca Tranchini)"
   Paolo PISTONE (Université de Bologne)
  
  Résumé : The "categorification" of proof systems is a recurrent theme in last years research. This approach aims at developing a new understanding of proof systems within the language of so-called higher-dimensional categories (that is, categories in which one can have arrows between arrows, arrows between arrows between arrows and so on).
  While most proof systems can be presented as categories of finite dimension, it is well-known that Martin-Löf's Intuitionistic Type Theory generates, under certain hypotheses, a category of infinite dimension. In this talk we suggest that Peter Schroeder-Heister's 1984 extension of natural deduction with higher-level rules yields another proof system HLR having infinite dimension. Moreover, we will show that HLR, seen as an infinitely dimensional type theory, can be used as a convenient meta-theory to investigate properties of proof systems like normalization and identity of proof.
  
  À noter : La séance de questions qui suivra aura lieu en français (de même, peut-être, que l’exposé lui-même).