[ITP 2026] BARReL

Zenodo (CERN European Organization for Nuclear Research) 2026 Open access

Read full text
Authors: Vincent Trélat, Ghilain Bergeron
DOI: 10.5281/zenodo.18137311
Cited by: 0

Abstract

BARReL: B Automated tRanslation for Reasoning in Lean BARReL bridges Atelier B proof obligations to Lean. It parses .pog files (the PO XML format produced by Atelier B), converts the obligations into Lean terms, and lets you discharge them with Lean tactics.

Publication details

Journal / source
Zenodo (CERN European Organization for Nuclear Research)
Publication date
3 January 2026
Language
EN