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 readable and computable formalization of the Streamlet consensus protocol
May 2025 — Mauro Jaskelioff, Orestis Melkonian, James Chapman
FMBC '25Validity, Liquidity, and Fidelity: Formal Verification for Smart Contracts in Cardano
May 2025 — Tudor Ferariu, Prof Philip Wadler, Orestis Melkonian
FMBC '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 '24Reasonable Agda Is Correct Haskell: Writing Verified Haskell using agda2hs
September 2022 — Jesper Cockx, Orestis Melkonian, Lucas Escot, James Chapman, Ulf Norell
Haskell '22A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs
October 2021 — Guillame Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
Journal of Functional ProgrammingNative Custom Tokens in the Extended UTXO Model
October 2020 — Manuel Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Jann Müller, Michael Peyton Jones, Polina Vinogradova, Prof Philip Wadler
UTXOma:UTXO with Multi-Asset Support
October 2020 — Manuel Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Jann Müller, Michael Peyton Jones, Polina Vinogradova, Prof Philip Wadler, Joachim Zahnentferner