Sambo Boris ENG

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

Look at the front page for email

## Scientific interests

- Foundations of Logic and Computation
- Linear Logic, Proof-nets, Geometry of Interaction, Transcendental Syntax
- Non-classical approaches to Computational Complexity

## Education

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 |

## Experience

**Université Paris 13 – LIPN (LoVe team).**Supervised by Damiano Mazza and Thomas Seiller. Villetaneuse, France (October 2019 – Now).

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

**Université Paris 13 – LIPN (LoVe team).**Supervised by Thomas Seiller. Villetaneuse, France (March – August 2019).

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.

**Université Paris 13 – LIPN (LoVe team).**Supervised by Damiano Mazza. Villetaneuse, France (February – July 2018).

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

**Université Paris 7 – IRIF.**Supervised by Delia Kesner and Michele Pagani. Paris, France (June 2017, 8 weeks).

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.

**Inria de Paris (PROSECCO team).**Supervised by Yannis Juglaret. Paris, France (April 2016, 12 weeks).

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.

## Teaching

- Université Sorbonne Paris Nord 2020/2021
**Foundations of programming**(First year of Master in Computer Science, 21h): abstract machines (counter machines, SRAM, PRAM), pure and typed lambda-calculus, term rewriting**Introduction to programming**(First year in Mathematics/Computer Science, 27h): introduction to the C language

- Université Sorbonne Paris Nord 2019/2020
**Introduction to programming**(First year in Physics/Chemistry/Engineering, 27h): introduction to the C language**Logic**(First year in Computer Science, 18h): proof by induction, truth tables, sequent calculus, lambda-calculus**Functional programming**(Second year in Computer Science, 15h): introduction to OCaml, lambda-calculus

## Publications

- Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation (April 2016) with Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Benjamin C. Pierce. CSF 2016.

## Conferences attended

- FSCD 2020, June-July 2020, Paris (France). Online conference.
- 29th IEEE Symposium on Computer Security Foundations (CSF), July 2016, Lisbon (Portugal). IEEE Student Travel Grant.

## Skills

Programming |
OCaml, Java, C, C++, Python |

Formal methods |
Coq |

Project management |
Git, Make |

Web |
HTML, CSS |

Others |
LaTeX, TikZ |

## Languages

French |
Mother tongue |

English |
Fluent in written English, can communicate in spoken English but not used to it |