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 In the proceedings of Topics in Cryptology -- CT-RSA 2021, 2021
Preprint available at IACR
Download here
Threshold Schnorr with Stateless Deterministic Signing from Standard Assumptions
Published in In the proceedings of Advances in Cryptology -- CRYPTO 2021, 2021
Pre-print available at IACR
LURK: Lambda, the Ultimate Recursive Knowledge (Experience Report)
Published in In the proceedings of International Conference on Functional Programming, 2023
Pre-print available at IACR
Subset-Optimized BLS Multi-signature with Key Aggregation
Published in In the proceedings of Financial Cryptography and Data Security. FC 2024, 2025
Preprint available at IACR
Download here
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.
Scaling the Celo Blockchain with Narwhal
Published:
This talk presents work in integrating the Narwhal mempool and Bullshark consensus protocol in the Celo blockchain
Groth16 still lives: exploring the trade-offs of modern ZKProof systems
Published:
In October 2019, on the heels of SNARK-tember, Georgios Konstantopoulos gave a well-received talk exploring the tradeoff space of ZKP Systems, titled “Groth16 is not dead”.
Taming the Many EddSAs
Published:
In this talk we will discuss the security of concrete instantiations of EdDSA by identifying exploitable inconsistencies between standardization recommendations and Ed25519 implementations. We will mainly focus on current ambiguity regarding signature verification equations, binding and malleability guarantees, and incompatibilities between randomized batch and single verification. Based on our work that appeared at SSR 2020, we will give a formulation of the Ed25519 signature scheme that achieves the highest level of security, explaining how each step of the algorithm links with the formal security properties.
Lambda the Ultimate Recursive Knowledge
Published:
We introduce Lurk, a groundbreaking LISP-based programming language for zk-SNARKs. Unlike conventional approaches that involve compiling computations into flat circuits, Lurk allows programs to be provided as data to the universal Lurk interpreter circuit. This innovative design empowers Lurk with Turing-completeness, without sacrificing the size of the resulting proof artifacts.
Nova ZK Proof Verification in the EVM
Published:
We introduce the challenges of writing a verifier for the Nova ZKP system on Ethereum, and the methods used to overcome those challenges.
Lurk: Lambda, the Ultimate Recursive Knowledge
Published:
We introduce Lurk, a new LISP-based programming language for zk-SNARKs. Traditional approaches to programming over zero-knowledge proofs require compiling the desired computation into a flat circuit, imposing serious constraints on the size and complexity of computations that can be achieved in practice. Lurk programs are instead provided as data to the universal Lurk interpreter circuit, allowing the resulting language to be Turing-complete without compromising the size of the resulting proof artifacts. Our work describes the design and theory behind Lurk, along with detailing how its implementation of content addressing can be used to sidestep many of the usual concerns of programming zero-knowledge proofs.
Front-Running the Aggregate: Proofcoin as a New Paradigm for Security and Flexibility
Published:
Proofcoin, a next-generation decentralized Layer 2 solution with an Ethereum backstop, redefines how proof aggregation can enhance security without compromising user flexibility. In this talk, we’ll explore how Proofcoin employs aggregation, not for programmability, but as a foundation for security. Rather than relying on aggregated proofs as a programming model, Proofcoin provides users with proof certificates that they can work with directly, effectively front-running the aggregate.