Skip to main content

Search

Show all results for

Home

Person

Aurèle Aimé Aubin Barrière

About
Privacy
Disclaimer

Copyright © 2025 EPFL, all rights reserved

Graph Chatbot

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications (3)

Please note that this is not a complete list of this person’s publications. It includes only semantically relevant works. For a full list, please refer to Infoscience.

Courses taught by this person (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

Related units (1)

Systems and Formalisms lab

EPFL
IC
IINFCOM
SYSTEMF

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