Program Extraction from Large Proof Developments

DOI10.1007/10930755_14zbMath1279.68287OpenAlexW2096282101MaRDI QIDQ3559767

Bas Spitters, Luís Cruz-Filipe

Publication date: 7 May 2010

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/10930755_14

zbMATH Keywords

constructive mathematicsprogram extractiontype theoryformalized mathematics

Mathematics Subject Classification ID

Related Items (5)

Code-carrying theories ⋮ Extracting functional programs from Coq, in Coq ⋮ Certified Exact Transcendental Real Number Computation in Coq ⋮ A computer-verified monadic functional implementation of the integral ⋮ Computer Certified Efficient Exact Reals in Coq

Uses Software

• Coq

This page was built for publication: Program Extraction from Large Proof Developments