CV › Boris Eng

Boris Eng

ATER at Université Sorbonne Paris Nord, France

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

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

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.

Master internship at 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.

Research project at 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).

Internship at 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.

Internship at 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 2021/2022
- Introduction to programming (First year in Mathematics/Computer Science, 27h): introduction to the C language.
- Introduction to computability (Third year in Computer Science, 19.5h): countable sets, counter machines, decision problems, Turing machines, recursively enumerable sets.
Université Sorbonne Paris Nord 2020/2021
- Foundations of programming (1st year of Master in Computer Science, 21h): abstract machines (counter, SRAM, PRAM), pure/typed lambda-calculus.
- Introduction to programming (First year in Mathematics/Computer Science, 27h): introduction to the C language.
- Functional programming (Second year in Computer Science, 15h): lambda-calculus, encodings, types, term unification, type inference.
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 semantics, sequent calculus, typed lambda-calculus.
- Functional programming (Second year in Computer Science, 15h): introduction to OCaml.

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.
A gentle introduction to Girard’s Transcendental Syntax (June 2021) with Thomas Seiller. TLLA 2021 (workshop).

Research school attended

CIRM 2022 Logic and Transdisciplinarity, February 2022, Marseille.
CIRM 2022 Linear Logic Winter School, January 2022, Marseille.
ISR 2021, July 2021, Midlands (online).
MGS 2021, April 2021, Midlands (online).
EJCIM 2020, June 2020, Bordeaux (online).

Conferences attended

“Trends in Linear Logic and Applications” TLLA 2021 (online).
GT SCALP 2021, November 2021, Fontainebleau (France).
29th IEEE Symposium on Computer Security Foundations (CSF), July 2016, Lisbon (Portugal). IEEE Student Travel Grant.

Skills

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

Languages

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