Meetings

• Artificial intelligence and formal proofs
  Luc Pommeret · 40min

Organized by Jérémy Hervé, Boris Eng, Victor Benitah

By Pierre Cardascia

• Morts du mythe, de l'art, de la philosophie, de la logique : Itinéraire d'un problème serial-killer
  Pierre Cardascia · 1h30

By Boris Eng and Pablo Donato

By Luc Pommeret

• Le professionnel et l'écrivain : le pouvoir offensif de la philosophie analytique
  Luc Pommeret · 1h30

• Introduction to Peirce's philosophy
  Pablo Donato · 30min
• Stellar resolution and Girard's knitting
  Boris Eng

By Xavier Denis

• Presentation of the Rust programming language
  Xavier Denis · 1h
• Why formal verification is getting it wrong
  Xavier Denis · 1h

By Kostia Chardonnet

Chair: Kostia Chardonnet

• Quantum computation and Geometry of Interaction
  Kostia Chardonnet · 45min

By Tito and Valentin Maestracci

Chair: Pablo Donato

• Pourquoi les catégories sont la bonne façon de faire de la sémantique dénotationnelle
  Tito · 1h
• Catégories monoïdales à trace
  Valentin Maestracci · 1h

By Pablo Donato, Davide Barbarossa, Adrien Ragot, Boris Eng, Sidney Congard

Chair: Boris Eng

• Du calcul des séquents à la logique linéaire
  Pablo Donato · 30min
• Correspondance de Curry-Howard et théorie des types
  Davide Barbarossa · 30min
• Réseaux de preuve multiplicatifs avec règle daemon
  Adrien Ragot · 30min
• Introduction à la géométrie de l'interaction originale de Girard
  Boris Eng · 30min
• Introduction à la syntaxe transcendantale
  Sidney Congard · 30min

• Apodictic and Epidictic in Girard's transcendental syntax. Control over computation (synchronicity, sequentiality, direction of computation).

By Pablo Donato

• Comparison between deep inference and proof-nets. Non-sequentialisable multiplicative connectives, ludics, proof assistants, sequent calculi as recipes for computational objects (constellations).

By Boris Eng

• Discussion on stellar resolution and ways to put meaning on it (Girard's "usine" and "usage"), correctness criterion, realisability theory.

By Boris Eng and Julien Marquet

• Discussion on possible encodings of lambda-calculus and Lafont's interaction nets with unification (by using stellar resolution). Decomposition of tests as constellations. Discussions on optimal reduction of lambda-calculus.

• Discussions on Girard's transcendental syntax. Focus on Girard's "conceptual knitting".