François Garillot

François Garillot

Research engineer and coffee fan.

Posts by Tags

Coq

Certifying RSA correct for breakfast

7 minute read

Published:

Reasoning on the correctness of the RSA cryptosystem is much easier with a little bit of algebra: this is a perfect example of a case where the ``practical’’ applications of proof assistants can be helped with libraries dealing with abstract algebra, including SSReflect. The proof we are going to build in the present post is based on a stock SSReflect version 1.3pl1, and is available on github. It can be compared with the RSA contribution to Coq, made on the basis of the standard library (note this is not a code golf, but rather a tentative to demonstrate that a big mathematical library helps).

Ligtweight profiling for your Coq hacks

3 minute read

Published:

Let’s suppose we want to hack a few functions in the Coq compiler. The classic situation is that we have the base implementation of our function as it stands, and an optimized version for which we want to check it really improves things.

EFI

Mac

Python

How do you make a recursive merge sort more efficient in Python?

5 minute read

Published:

This is re-worked from an excerpt of an answer of mine (1) to an SO question that made me discover some interesting things about Python : turns out it’s not easy to make recursion faster by doing tail call elimination, even by hand. (2)

  1. Initially fraught with errors, and therefore duly ill-scored. ↩

  2. This has also benefited a lot of a discussion with Carey Underwood below and in a reddit thread on this post. Many thanks ! ↩

RSA

Certifying RSA correct for breakfast

7 minute read

Published:

Reasoning on the correctness of the RSA cryptosystem is much easier with a little bit of algebra: this is a perfect example of a case where the ``practical’’ applications of proof assistants can be helped with libraries dealing with abstract algebra, including SSReflect. The proof we are going to build in the present post is based on a stock SSReflect version 1.3pl1, and is available on github. It can be compared with the RSA contribution to Coq, made on the basis of the standard library (note this is not a code golf, but rather a tentative to demonstrate that a big mathematical library helps).

Ramdisk

Scala

Every freshman CS question in ±80 lines of Scala

14 minute read

Published:

This post is about writing a single program that returns the stream representing any recursive sequence of order $k$, which $i$th term a[i] = f(a[i-1], a[i-2], ... a[i-k]), for all $k$, in Scala. It explains things very slowly: If the meaning of the previous sentence is already 100% clear to you, you can easily skip the next 2 paragraphs.

Xen

apache

apache spark

A quick update on Spark Streaming work

3 minute read

Published:

Since I was asked a few times here at Scala Days, I thought I’d write an update on how some of our work on making Spark Streaming more resilient is going. Naturally, all of this is open-source, otherwise I wouldn’t be writing this.

archlinux

backpressure

A quick update on Spark Streaming work

3 minute read

Published:

Since I was asked a few times here at Scala Days, I thought I’d write an update on how some of our work on making Spark Streaming more resilient is going. Naturally, all of this is open-source, otherwise I wouldn’t be writing this.

big data

May 2016 time series storage roundup

1 minute read

Published:

A recent slew of blogs and articles have been shedding new insight on time series storage. I thought I’d list some of the zeitgeist.

data science

deep learning

formal-methods

Certifying RSA correct for breakfast

7 minute read

Published:

Reasoning on the correctness of the RSA cryptosystem is much easier with a little bit of algebra: this is a perfect example of a case where the ``practical’’ applications of proof assistants can be helped with libraries dealing with abstract algebra, including SSReflect. The proof we are going to build in the present post is based on a stock SSReflect version 1.3pl1, and is available on github. It can be compared with the RSA contribution to Coq, made on the basis of the standard library (note this is not a code golf, but rather a tentative to demonstrate that a big mathematical library helps).

level

Look, Ma, no queues!

4 minute read

Published:

A very classic, if a bit overrated exercise, is to print a tree in width-first order. Also called level-order, it means you print your binary tree row-by-row, with the nodes of depth d, leftmost first, before the nodes of depth d+1.

maven

PSA: maven central and sonatype are slow

less than 1 minute read

Published:

Most of the public maven repositories for downloading java artifacts (notably maven-central, and sonatype) are slow. Besides, build tools do not have a perfect track record of resolving dependencies from these repositories in an efficient manner.

merge-sort

How do you make a recursive merge sort more efficient in Python?

5 minute read

Published:

This is re-worked from an excerpt of an answer of mine (1) to an SO question that made me discover some interesting things about Python : turns out it’s not easy to make recursion faster by doing tail call elimination, even by hand. (2)

  1. Initially fraught with errors, and therefore duly ill-scored. ↩

  2. This has also benefited a lot of a discussion with Carey Underwood below and in a reddit thread on this post. Many thanks ! ↩

monad

monad transformer

nexus

PSA: maven central and sonatype are slow

less than 1 minute read

Published:

Most of the public maven repositories for downloading java artifacts (notably maven-central, and sonatype) are slow. Besides, build tools do not have a perfect track record of resolving dependencies from these repositories in an efficient manner.

overlapping-implicits

Every freshman CS question in ±80 lines of Scala

14 minute read

Published:

This post is about writing a single program that returns the stream representing any recursive sequence of order $k$, which $i$th term a[i] = f(a[i-1], a[i-2], ... a[i-k]), for all $k$, in Scala. It explains things very slowly: If the meaning of the previous sentence is already 100% clear to you, you can easily skip the next 2 paragraphs.

profiling

Ligtweight profiling for your Coq hacks

3 minute read

Published:

Let’s suppose we want to hack a few functions in the Coq compiler. The classic situation is that we have the base implementation of our function as it stands, and an optimized version for which we want to check it really improves things.

queues

Look, Ma, no queues!

4 minute read

Published:

A very classic, if a bit overrated exercise, is to print a tree in width-first order. Also called level-order, it means you print your binary tree row-by-row, with the nodes of depth d, leftmost first, before the nodes of depth d+1.

recursion

How do you make a recursive merge sort more efficient in Python?

5 minute read

Published:

This is re-worked from an excerpt of an answer of mine (1) to an SO question that made me discover some interesting things about Python : turns out it’s not easy to make recursion faster by doing tail call elimination, even by hand. (2)

  1. Initially fraught with errors, and therefore duly ill-scored. ↩

  2. This has also benefited a lot of a discussion with Carey Underwood below and in a reddit thread on this post. Many thanks ! ↩

streaming

A quick update on Spark Streaming work

3 minute read

Published:

Since I was asked a few times here at Scala Days, I thought I’d write an update on how some of our work on making Spark Streaming more resilient is going. Naturally, all of this is open-source, otherwise I wouldn’t be writing this.

time series

May 2016 time series storage roundup

1 minute read

Published:

A recent slew of blogs and articles have been shedding new insight on time series storage. I thought I’d list some of the zeitgeist.

xml

PSA: maven central and sonatype are slow

less than 1 minute read

Published:

Most of the public maven repositories for downloading java artifacts (notably maven-central, and sonatype) are slow. Besides, build tools do not have a perfect track record of resolving dependencies from these repositories in an efficient manner.