Sambo Boris ENG

PhD student in Computer Science at LIPN - LoVe Team (Université Paris 13)

Please ask for address | Please ask for phone number |

Scientific interests


Degree School Year
PhD in Computer Science Université Paris 13 2019–Now
Master Parisien de Recherche en Informatique (MPRI) Université Paris 7 2018–2019
Master 1 Informatique Recherche (15.5/20, mention B) Université Paris 7 2017–2018
Licence 3 Informatique (Rang 2, Rang 1, mention TB) Université Paris 7 2016–2017
DUT Informatique (Rang 1) IUT de Montreuil 2014–2016
Baccalauréat Technologique STI2D (Mention B) Lycée Dorian 2011–2014


Investigations on the time and space complexity of functional programs (lambda-calculus) through polyadic approximations (affine approximations of programs) and the Geometry of Interaction. Works on the lambda-calculus as a reasonable cost model. Formalization of the "Transcendental Syntax" project of Jean-Yves Girard (definition of MLL and eventually exponentials, second order and first-order through Unification Theory).
Formalisation of the Transcendental Syntax project of Jean-Yves Girard for Multiplicative Linear Logic (MLL). Definition of a computational model "stars and constellations" based on first-order term unification which is able to simulate proof-nets, cut elimination, formulas but also the correctness criterion of Danos-Regnier. Formal definitions are provided with a proof of confluence for the execution of constellations. The model is also connected to the program of Geometry of Interaction.
Investigations on the space complexity of functional programs. Use of tools from implicit complexity (geometry of interaction, intersection types and linear logic) and the approximation of Turing machines into uniform families of circuits transposed into the lambda-calculus through the idea of "polyadic approximation". It is a step in the view of the lambda-calculus as a reasonable cost model (relatively close to Turing machine's complexity).
Translation of the PCF language (Turing-complete extension of the lambda-calculus with booleans, natural numbers and fixpoint operator) into linear logic’s proof nets extended to the explicit substitution calculus “Linear Substitution Calculus”. Proof of a property of simulation showing the correspondence between the reductions of the terms of PCF and cut-elimination procedure of proof nets.
Modelisation of an abstract machine, a compiler linking two toy languages (close to the C language and an assembly language) and proof of various properties related to the operational semantics and the typing (Partial Type Safety) of the source language using Coq. Formal verification of the security guarantee "Secure Compartmentalizing Compilation" suggested in the context of the Secure Compilation project.



Conferences attended


Programming OCaml, Java, C, C++, Python
Formal methods Coq
Project management Git, Make
Others LaTeX, TikZ


French Mother tongue
English Fluent in written English, can communicate in spoken English but not used to it