HTTP/2 200 date: Sun, 18 Jan 2026 01:53:17 GMT content-type: text/html content-length: 3658 server: OVHcloud accept-ranges: bytes vary: Accept-Encoding content-encoding: gzip

I am a maître de conférences at Nantes Université, working in the Gallinette team of the LS2N.

Email:

guilhem.jaber -at- univ-nantes.fr

Publications

• Operational game semantics for generative algebraic effects
  with Hamza Jaafar
  PPDP'25
  
• An abstract, certified account of operational game semantics
  with Peio Borthelle, Tom Hirschowitz, and Yannick Zakowski
  ESOP'25
  
• Deciding contextual equivalence of ν-calculus with effectful contexts (full version)
  with Daniel Hirschkoff and Enguerrand Prebet
  FoSSaCS'23
  
• Games, Mobile Processes, and Functions (full version)
  with Davide Sangiorgi
  CSL'22
  
• Theorems for free from separation logic specifications
  with Lars Birkedal, Thomas Dinsdale-Young, Armael Gueneau, Kasper Svendsen and Nikos Tzevelekos
  ICFP'21 - Distinguished Paper Award
  
• Compositional relational reasoning via operational game semantics
  with Andrzej Murawski
  LICS'21
  
• Complete trace models of state and control (full version)
  with Andrzej Murawski
  ESOP'21
  
• Temporal Refinements for Guarded Recursive Types (full version)
  with Colin Riba
  ESOP'21
  
• SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References
  POPL'20, New Orleans
  
• A Trace Semantics for System F Parametric Polymorphism
  with Nikos Tzevelekos
  FoSSaCS'18, Thessaloniki
  
• The Definitional Side of Forcing
  with Gabriel Lewertowski, Matthieu Sozeau, Pierre-Marie Pedrot and Nicolas Tabareau
  LICS'16, New York
  
• Trace Semantics for Polymorphic References
  with Nikos Tzevelekos
  LICS'16, New York
  
• A Kripke logical relation for effect-based program transformations
  with Lars Birkedal, Filip Sieczkowski and Jacob Thamsborg
  Information and Computation 249, 160-189, 2016
  
• Kripke Open Bisimulation: A Marriage of Game Semantics and Operational Techniques
  with Nicolas Tabareau
  APLAS'15, Pohang
  
• Operational Nominal Game Semantics
  FoSSaCS'15, London
  
• Extending Type Theory with Forcing
  with Nicolas Tabareau and Matthieu Sozeau
  LICS'12, Dubrovnik
  
• The Journey of Biorthogonal Logical Relations to the Realm of Assembly Code
  with Nicolas Tabareau
  LOLA'11 (LICS workshop), Toronto
  
• Krivine Realizability for Compiler Correctness
  with Nicolas Tabareau
  LOLA'10 (LICS workshop), Edinburgh
  
• A Computational Interpretation of Forcing in Type Theory
  with Thierry Coquand
  Epistemology versus Ontology Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf, Springer (2012)
  
• A Note on Forcing and Type Theory
  with Thierry Coquand
  Fundamenta Informaticae 100(1-4): 43-52 (2010)
  

Current supervision

• Matteo Spadetto - Postdoc on the ReCiProg project
• Hamza Jaafar - PhD student on the CAVOC project

Former supervision

• Axel Kerinec - (Sept. 2023 - Aug. 2025) - Postdoc on the CANofGAS project - Now Postdoc at LACL
• Peio Borthelle - PhD student, co-advised with Tom Hirschowitz and Yannick Zakowski - (defended on 3rd September 2025)

Research grants

• RECIPROG, (Reasoning on Circular Proofs for Programming) - ANR PRC Project - 2021-2025 - Nantes local coordinator
• CAVOC (Compositional Automated Verification of OCaml Code) - Inria-Nomadic Labs research agreement - 2021-2025 - Project Investigator
• CANofGAS (Cost Analysis of Game Semantics) - Inria Exploratory Action - 2022-2025 - Project Co-Investigator with Beniamino Accattoli

Service

HOPE'25 (co-chair), LICS'25 (PC member), HOPE'24 (co-chair), POPL'24 (PC member), FICS'24 (PC member), MFPS'23 (PC member), ESOP'22 (PC member)

PhD thesis

• A Logical Study of Program Equivalence
  supervised by Nicolas Tabareau and Alexandre Miquel
  defended on 2014-07-11 at Institut Henri Poincare (Slides)