Extracting Imperative Programs from Proofs: In-place Quicksort

DOI10.4230/LIPICS.TYPES.2013.84zbMath1359.68042OpenAlexW1522541548MaRDI QIDQ2968412

Monika Seisenberger, Ulrich Berger, Gregory J. M. Woods

Publication date: 13 March 2017

Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2014/4627/pdf/p084-05-berger.pdf

zbMATH Keywords

verificationrealizabilityprogram extractionimperative programscomputational monadsMinlogIn-place Quicksort

Mathematics Subject Classification ID

Searching and sorting (68P10) Functional programming and lambda calculus (68N18)

Related Items (3)

Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs

Uses Software

• Minlog

This page was built for publication: Extracting Imperative Programs from Proofs: In-place Quicksort