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