Sambo Boris ENG

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

Please ask for address | Please ask for phone number | engboris@hotmail.fr

## 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

**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

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