Passer au contenu principal

Recherche

Afficher tous les résultats pour

Accueil

Personne

Aurèle Aimé Aubin Barrière

À propos
Confidentialité
Mentions légales

Copyright © 2025 EPFL, tous droits réservés

Graph Chatbot

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Cours enseignés par cette personne (1)

CS-428: Interactive theorem proving

A hands-on introduction to interactive theorem proving, computer-checked mathematics, compiler verification, proofs as programs, dependent types, and proof automation. Come learn how to write compute

Publications associées (3)

Veuillez noter qu'il ne s'agit pas d'une liste complète des publications de cette personne. Elle inclut uniquement les travaux sémantiquement pertinents. Pour une liste complète, veuillez consulter Infoscience.

Formal Verification of Just-in-Time Compilation

Aurèle Aimé Aubin Barrière

This book outlines a methodology to develop formally verified Just-in-Time compilers. Just-in-Time compilation is a technique to execute programs, where execution is interleaved with optimizations of the program itself. These compilers often produce fast e ...

Association for Computing Machinery2025

A Coq Mechanization of JavaScript Regular Expression Semantics

Clément Pit-Claudel, Aurèle Aimé Aubin Barrière

We present an executable, proven-safe, faithful, and future-proof Coq mechanization of JavaScript regular expression (regex) matching, as specified by the latest published edition of ECMA-262 section 22.2. This is, to our knowledge, the first time that an ...

2024

Linear Matching of JavaScript Regular Expressions

Clément Pit-Claudel, Aurèle Aimé Aubin Barrière

Modern regex languages have strayed far from well-understood traditional regular expressions: They include features that fundamentally transform the matching problem. In exchange for these features, modern regex engines at times suffer from exponential com ...

2024

Unités associées (1)

Laboratoire systèmes et formalismes

EPFL
IC
IINFCOM
SYSTEMF