Écriture en Coq d'une sémantique d'un interpréteur d'une sous partie de Rust et C. Cet interpreteur selon certaines conditions assurent les préconditions du Rust même lors de l'exécution de code C sur les structures de données Rust.
Ecriture d'une sémantique et d'un système de type pour une partie du langage Rust sous la direction de David Baelde en parallèle de mes cours de Master 1. L'objectif étant d'assurer des propriétés de Borrow checking. Travail réutilisé dans un cours de Licence d'introduction au Rust.
Travaille sur le projet HyperAST de l'équipe de recherche DIVERSE. Cette structure de donnée permet d'analyser des historiques git. A chaque commit est associé un AST, l'HyperAST prend en compte le temps pour stocker une image complète d'un projet ce qui permet une analyse plus rapide.
Cours : Apprentissable, IA, Langage Formel, Programmation Théorique et Compilation, Sémantique (Logique, Lambda Calcul), Calculabilité, Architectures, Réseaux, Systèmes d'exploitations, Algorithmique, Bases de données.
Cours : Logique et représentation des connaissances, Machine Learning, Compilation, Philosophie et Espitémologie, Théorie de l'information, Logique Avancée, Parallel programming, Advanced Operating System.
Cours : Algorithmiques, Programmation C, Ocaml et C++, Cryptographie, Logique, Architecture et Système, Calculabilité, Sémantique et preuve de programme, Analyse d'images, Théorie de la complexité.
Cours : Intégration de Lesbegues, Théorie des groupes, Probabilité et Statistiques, Anneaux et Corps, Topologie Générale, Calcul Différentiel, Optimisation, Espaces vectoriels normés.
Cours : Mathématique (Algèbre, Probabilités, Calcul Intégral, Analyse, Equations Différentielles), Physique (Mécanique classique, Physique Quantique, Electromagnétisme, Mécanique Statistiques, Physique des particules, Chimie), Informatique (Programmation Ocaml, Théorie des graphes).
Theoretical semantics of an interpreteur of both C and Rust (simplified version). This simple interpreter assures good behavior even for C and Rust code changing shared structures of data.
Establish the semantics of a small subset of Rust under the supervision of David Baelde. Writing a type checker and a borrow checker for this language. Proof that if a program types, then it does not have any memory errors during execution.
Work on the HyperAST project with the DIVERSE research team. This tool in development aims at analyzing git history in a more efficient way. For each commit we get an AST, the HyperAST takes the time into account to store a complete image of a complete git history that can be searched faster than any other state-of-the-art method.
Cours : Machine Learning, Automata Theory, Programming Langage Theory, Compilation, Parsing, Sémantics, Lambda Calculus, Calculability, Computer Architecture, Networks, Operating Systems, Algorithmics, Database Theory.
Cours : Logic and Knowledge Representation, Machine Learning, General Compiler Concept, Philosophy and Epistemology, Information Theory, Programmation Parallèle, Systèmes d'exploitations.
Cours : Advanced Algorithm, Programming in C, Ocaml and C++, Cryptography, Logic, Architecture and System, Theory of Computability, Semantics and proof assistants, Image and Signal Processing, Complexity Theory.
Cours : Lebesgue Integration, Group Theory, Statistics and Probability, Rings and Arithmetic, General Topology, Differential Calculus, Optimisation, Normed Vector Spaces.
Cours : Mathematics (Algebra, Probability, Integral calculus, Analysis, Differential equation), Physics (Classical Mechanics, Quantum Mechanics, Electromagnetism, Statistical Mechanics, Quantum Field Theory, Particle Physics), Computer Science (Ocaml programming, Graph theory).