Boris Eng

ATER at Université Sorbonne Paris Nord, France

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


Exegesis of Girard's Transcendental Syntax extending a first formalisation with Thomas Seiller. Full definition of the stellar resolution, the model of computation used as a ground for logic, investigations on the links between the Transcendental Syntax and other subjects (tile systems, asynchronous models of computation, model checking, type theory). Extensions to exponentials and sketching of further extensions.
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.



Research school attended

Conferences attended


Programming OCaml, Haskell, Java, C, C++, Python
Formal methods Coq
Project management Git, Make
Web HTML, CSS, Jekyll
Others LaTeX, TikZ


French Mother tongue
English Fluent in written English, can communicate in spoken English