Articles liés

Articles écrits par Guillaume Bury

Site

Catégories

Flambda2 Ep. 3: Speculative Inlining

Auteurs: Pierre Chambart, Vincent Laviron, Guillaume Bury, Dario Pinto, Nathanaëlle Courant
Date: 2024-08-09
Catégorie: OCaml
Tags: flambda2, flambda, compiler, optimisation, f2s, inlining

Welcome to a new episode of The Flambda2 Snippets! The F2S blog posts aim at gradually introducing the world to the inner-workings of a complex piece of software engineering: The Flambda2 Optimising Compiler for OCaml, a technical marvel born from a 10 year-long effort in Research & Development and ... (Lire plus)

Flambda2 Ep. 2: Loopifying Tail-Recursive Functions

Auteurs: Nathanaëlle Courant, Guillaume Bury, Pierre Chambart, Vincent Laviron, Dario Pinto
Date: 2024-05-07
Catégorie: OCaml
Tags: Flambda, Flambda2, loopify, optimisation, f2s, ep2, loopify, tailcall, tail-recursion

Welcome to a new episode of The Flambda2 Snippets! Today's topic is Loopify, one of Flambda2's many optimisation algorithms which specifically deals with optimising both purely tail-recursive and/or functions annotated with the [@@loop] attribute in OCaml. A lazy explanation for its utility would be... (Lire plus)

Flambda2 Ep. 1: Foundational Design Decisions

Auteurs: Pierre Chambart, Vincent Laviron, Guillaume Bury, Nathanaëlle Courant, Dario Pinto
Date: 2024-03-19
Catégorie: OCaml
Tags: flambda2, flambda, compiler, optimization, cps, f2s, ep1

Welcome to The Flambda2 Snippets! In this first post of The Flambda2 Snippets, we dive into the powerful CPS-based internal representation used within the Flambda2 optimizer, which was one of the main motivation to move on from the former Flambda optimizer. Credit goes to Andrew Kennedy's paper Comp... (Lire plus)

Release of ocplib-simplex, version 0.5

Auteurs: Steven de Oliveira, Pierre Villemot, Hichem Rami Ait El Hara, Guillaume Bury
Date: 2023-01-05
Catégorie: Formal Methods
Tags: OCaml, alt-ergo, simplex, ocplib

On last November, we released version 0.5 of ocplib-simplex, a generic library implementing the Simplex Algorithm in OCaml. It is a key component of the Alt-Ergo automatic theorem prover that we keep developing at OCamlPro. ** The Simplex Algorithm What Changed in 0.5 ? ] The simplex algorithm The S... (Lire plus)

Alt-Ergo: the SMT solver with model generation

Auteurs: Steven de Oliveira, Pierre Villemot, Hichem Rami Ait El Hara, Guillaume Bury
Date: 2022-11-16
Catégorie: Formal Methods
Tags: OCaml, alt-ergo

The Alt-Ergo automatic theorem prover developed at OCamlPro has just been released with a major update : counterexample model can now be generated. This is now available on the next branch, and will officially be part of the 2.5.0 release, coming this year ! Alt-Ergo at a Glance Alt-Ergo is an open ... (Lire plus)