# Sitemap

A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.

## PSA: maven central and sonatype are slow

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.

## A June 2016 roundup of distributed Deep Learning projects on Apache Spark

Published:

Here’s a quick roundup of distributed deep learning efforts running on Apache Spark. This will only list active(-ish) projects rather than academic experiments (of which there are too many to list) There’s roughly two approaches:

## May 2016 time series storage roundup

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.

## Another update on streaming work

Published:

This is an update on my previous post about work by Typesafe to add resiliency to Spark Streaming.

## A quick update on Spark Streaming work

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.

## Diving In The Deep End of The Big Data Pool: Talk Abstract

Published:

This is the Abstract for my Ignite talk at the Strata+Hadoop Barcelona conference, on Wed Nov 19th, 2014 (at CCIB, room 116, 5:30PM). I haven’t found any place where O’Reilly would publish that abstract, and I thought some people would want a peek at what I’d talk about.

Published:

## Introduction

Published:

I’ve recently heard the following suprisingly general question:

## Look, Ma, no queues!

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.

## How a Ramdisk saved my life

Published:

… or how the devil finds work for idle hands.

## Every freshman CS question in ±80 lines of Scala

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.

## Certifying RSA correct for breakfast

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).

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

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 !

## Ligtweight profiling for your Coq hacks

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.

## Statically Typed Document Transformation: An Xtatic Experience

Published in In the proceedings of PLAN-X, 2006

Technical report version available at UPenn

## A core calculus for Scala type checking

Published in In the proceedings of International Symposium on Mathematical Foundations of Computer Science, 2006

Technical report available on HAL

## Simple types in type theory: Deep and shallow encodings

Published in In the proceedings of International Conference on Theorem Proving in Higher Order Logics, 2007

Access paper here

## Packaging mathematical structures

Published in In the proceedings of International Conference on Theorem Proving in Higher Order Logics, 2009

Technical report available on HAL

## Generic Proof Tools and Finite Group Theory

Published in Ecole Polytechnique X, 2011

My PhD Thesis work. If you're interested, you'll also want to dig into some older academic talks listed on my webpage at the ENS.

## A machine-checked proof of the odd order theorem

Published in In the proceedings of International Conference on Interactive Theorem Proving, 2013

Technical report accessible on HAL

## State machine replication in the Libra Blockchain

Published in The Diem Association, 2019

You can find a lot more information on Diem on the developer website.

## The Libra Blockchain

Published in The Diem Association, 2019

You can find a lot more information on Diem on the developer website.

## Taming the Many EdDSAs

Published in In the proceedings of Security Standardisation Research, 2020

Preprint available at IACR

## Non-interactive Half-Aggregation of EdDSA and Variants of Schnorr Signatures

Published in In the proceedings of Topics in Cryptology -- CT-RSA 2021, 2021

Preprint available at IACR

## Threshold Schnorr with Stateless Deterministic Signing from Standard Assumptions

Published in IACR, 2021

Accepted at Crypto 2021, Pre-print available at IACR

## Apache Mesos and Spark: Ramping Up your DevOps-Fu for Big Data Developers

Published:

A talk on the then-nascent Apache Spark distribution of Lightbend (then Typesafe) and the practices that allowed developing it fast.

## A Gentle Introduction to Spark and Locality Sensitive hashing

Published:

A talk on implementation and use cases for implementing efficient locality-sensitive hashing in Spark.

## Spark Streaming: Pushing the Throughput Limits, the Reactive Way

Published:

A talk on tuning a Spark Streaming cluster for performance.

## Spark Streaming: Dealing With State

Published:

A talk on dealing with state in Spark Streaming.

## Delivering near real time mobility insights at Swisscom

Published:

A use case developed at Swisscom to help urban planners understand their cities and to measure speeds on Swiss highways.

## Mobility Insights at Swisscom: Understanding Collective Mobility in Switzerland

Published:

An enterprise use case of analysing population movement data to improve mobility in Switzerland.

## DeepLearning4J and Spark: Success and Challenges

Published:

A talk about the challenges with using Deeplearning4J and Spark, in a distributed fashion.

## Deep Learning on a mixed cluster with DeepLearning4J and Spark

Published:

A talk co-located with NeurIPS 2016 on distributed deep learning in heterogeneous clusters.

## Growing Your Types Without Growing Your Workload, or How To Survive Among Productive Colleagues in Rust, or Defense Against the Dark Arts

Published:

This is a talk on how Rust derive macros make the eocnomics of some solutions to the expression problem simpler.

## Mechanized Proof for the Libra Blockchain

Published:

This talk presents formal methods work on the Diem (formerly Libra) blockchain, including a formalization of the safety of consensus in Coq.