DaanJamo/verified-pir: Thesis Version of the Verified Extraction Pipeline

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

Read full text
Authors: Daan de Munck, Jacco O.G. Krijnen, Wouter Swierstra
DOI: 10.5281/zenodo.18657494
Cited by: 0

Abstract

This release captures the state of our verified extraction pipeline at the time the thesis was submitted. It covers a subset of Gallina consisting of the simply-typed lambda-calculus with constant definitions. The term-level proof without globals is largely verified to be semantics preserving, the global translation and larger pipeline from Gallina to PIR is still unverified.

Fields of Study & Subjects

Logic programming and type systems Formal Methods in Verification Security and Verification in Computing

Publication details

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