Peregrine: a middle-end for code generation from proof assistants
May 2026 — Eske Hoy Nielsen, Simon Dima, Lucas Escot, Orestis Melkonian, Hugo Segoufin-Cholet, James Chapman, Yannick Forster, Matthieu Sozeau, Bas Spitters
Types '26Where science meets purpose
Categories
Topics
Authors
Research Papers
A Secure Sequencer and Data Availability Committee for Rollups (Extended Version)
October 2025 — Margarita Capretto, Martin Ceresa, Antonio Fernandez Anta, Pedro Moreno-Sanchez
ACM CCS '25Leakage-Free Probabilistic Jasmin Programs
January 2025 — José Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh
CPP '25Learning Structure-Aware Representations of Dependent Types
December 2024 — Konstantinos Kogkalidis, Orestis Melkonian, Jean-Philippe Bernardy
NeurIPS '24Applying Continuous Formal Methods to Cardano (Experience Report)
September 2024 — James Chapman, Arnaud Bailly, Polina Vinogradova
FUNARCH '24Flexible Formality: Practical Experience with Agile Formal Methods
August 2020 — Philipp Kant, Kevin Hammond, Duncan Coutts, James Chapman, Nicholas Clarke, Jared Corduan, Neil Davies, Javier Díaz, Matthias Güdemann, Wolfgang Jeltsch, Marcin Szamotulski, Polina Vinogradova