A Note on Forcing and Type Theory. - Thierry Coquand; Guilhem Jaber (Fundam. Informaticae, 2010)

Extending Type Theory with Forcing. - Guilhem Jaber; Nicolas Tabareau; Matthieu Sozeau (LICS, 2012)

A Computational Interpretation of Forcing in Type Theory. - Thierry Coquand; Guilhem Jaber (Epistemology versus Ontology, 2012)

A logical study of program equivalence. (Une étude logique de l'équivalence de programmes). - Guilhem Jaber (2014)

Kripke Open Bisimulation - A Marriage of Game Semantics and Operational Techniques. - Guilhem Jaber; Nicolas Tabareau (APLAS, 2015)

Operational Nominal Game Semantics. - Guilhem Jaber (FoSSaCS, 2015)

The Definitional Side of the Forcing. - Guilhem Jaber; Gabriel Lewertowski; Pierre-Marie Pédrot; Matthieu Sozeau; Nicolas Tabareau (LICS, 2016)

Trace semantics for polymorphic references. - Guilhem Jaber; Nikos Tzevelekos (LICS, 2016)

A Kripke logical relation for effect-based program transformations. - Lars Birkedal; Guilhem Jaber; Filip Sieczkowski; Jacob Thamsborg (Inf. Comput., 2016)

Trace Properties from Separation Logic Specifications. - Lars Birkedal; Thomas Dinsdale-Young; Guilhem Jaber; Kasper Svendsen; Nikos Tzevelekos (CoRR, 2017)

A Trace Semantics for System F Parametric Polymorphism. - Guilhem Jaber; Nikos Tzevelekos (FoSSaCS, 2018)

SyTeCi: automating contextual equivalence for higher-order programs with references. - Guilhem Jaber (Proc. ACM Program. Lang., 2020)

Complete trace models of state and control. - Guilhem Jaber; Andrzej S. Murawski (ESOP, 2021)

Temporal Refinements for Guarded Recursive Types. - Guilhem Jaber; Colin Riba (ESOP, 2021)

Compositional relational reasoning via operational game semantics. - Guilhem Jaber; Andrzej S. Murawski (LICS, 2021)

Theorems for free from separation logic specifications. - Lars Birkedal; Thomas Dinsdale-Young; Armaël Guéneau; Guilhem Jaber; Kasper Svendsen; Nikos Tzevelekos (Proc. ACM Program. Lang., 2021)

Games, Mobile Processes, and Functions. - Guilhem Jaber; Davide Sangiorgi (CSL, 2022)

Deciding Contextual Equivalence of ν-Calculus with Effectful Contexts. - Daniel Hirschkoff; Guilhem Jaber; Enguerrand Prebet (FoSSaCS, 2023)

An abstract, certified account of operational game semantics. - Peio Borthelle; Tom Hirschowitz; Guilhem Jaber; Yannick Zakowski (ESOP (1), 2025)

Artifact Report: an Abstract, Certified Account of Operational Game Semantics. - Peio Borthelle; Tom Hirschowitz; Guilhem Jaber; Yannick Zakowski (ESOP (1), 2025)