Guilhem Jaber

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

• 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)
  

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

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)