Statically Typed Document Transformation: An Xtatic Experience
Published in In the proceedings of PLAN-X, 2006
Technical report version available at UPenn
Download here
Posts by Collection
portfolio
publications
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
Download here
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
Download 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
Download here
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.
Download here
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
Download here
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.
Download here
The Libra Blockchain
Published in The Diem Association, 2019
You can find a lot more information on Diem on the developer website.
Download here
Stream Processing with Apache Spark
Published in O'Reilly Media, 2019
The book I co-wrote with Gérard Maas! I recommend finding a copy at your local book store.
Download here
Taming the Many EdDSAs
Published in In the proceedings of Security Standardisation Research, 2020
Preprint available at IACR
Download here
Non-interactive half-aggregation of EdDSA and variants of Schnorr signatures
Published in IACR e-prints, 2021
Accepted at CT-RSA 2021, Preprint available at IACR
talks
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.