Guilhem Jaber
I am a maître de conférences at Université de Nantes, working in the Gallinette team of the LS2N.
Previously, I was a PostDoc at LIP, in Lyon, in the Plume team, funded by the MILYON Labex.
I was a PostDoc at Université Paris 7, in the PPS team of IRIF,
working on the RAPIDO project with Alexis Saurin.
Before that, I was a PostDoc at the School of Electronic Engineering and Computer Science at
Queen Mary University, London, working under the supervision of Nikos Tzevelekos.
I have done my PhD at the École des Mines de Nantes in the Ascola Team, under the cosupervision of
Nicolas Tabareau
and Alexandre Miquel.
 Email:
 guilhem.jaber at univnantes.fr
News
Past News
 From the 26th to the 29th of December, I was in Bologna to work with Davide Sangiorgi on links between oeprational game semantics and picalculus.
 A new draft written with Colin Riba is available: Modal Logic of Transition Systems in the Topos of Trees.
 From the 20th to the 24th of May 2019, I have visited the Department of Computer Science at University of Oxford
to work with Andrzej Murawski.
 From the 17th to the 21st of December 2018, I have visited the Focus Team at University of Bologna
to work with Davide Sangiorgi.
 The 5th of December 2018, I have visited the Inria Prosecco team and gave a seminar there.
 I have participate to the Dagstuhl Seminar on Program Equivalence.
 I have given a talk at the 5th edition of the Languages, Compilation, and Semantics LIP Seminar.
 Our paper "A Trace Semantics for System F Parametric Polymorphism", written with Nikos Tzevelekos, has been accepted at FoSSaCS'18.
 A new draft is available:
Trace Properties from Separation Logic Specifications written with Lars Birkedal, Thomas DinsdaleYoung, Kasper Svendsen and Nikos Tzevelekos.
 I have participated to the Shonan Seminar on Enhanced Coinduction.
 I have given an invited presentation at
LOLA'16 the 10th of July in NewYork.
 I have served on the HOPE'16 Program Comitee.
 Two papers I have coauthored have been been published at LICS'16.
Research Interests
 Semantics of Programming Languages
Semantics of Assembly Code, Kripke Logical Relations, Game Semantics
 Formal Methods
Proof Assistants, Separation Logic, Static Analysis
 Foundations of Mathematics
Set Theory versus Type Theory, Topos theory, Axiom of Choice, Forcing
Publications
 SyTeCi: Automating Contextual Equivalence for HigherOrder 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, PierreMarie 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 effectbased program transformations
With Lars Birkedal, Filip Sieczkowski and Jacob Thamsborg
Information and Computation 249, 160189, 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 MartinLöf, Springer (2012)

A Note on Forcing and Type Theory
With Thierry Coquand
Fundamenta Informaticae 100(14): 4352 (2010)
PhD Thesis
Enseignements