Refinements for Free!
From MaRDI portal
Publication:2938045
DOI10.1007/978-3-319-03545-1_10zbMath1426.68165OpenAlexW2113181166MaRDI QIDQ2938045
Anders Mörtberg, Maxime Dénès, Cyril Cohen
Publication date: 13 January 2015
Published in: Certified Programs and Proofs (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01113453/file/refinements.pdf
Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (20)
A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Quotients of Bounded Natural Functors ⋮ Formalizing the Face Lattice of Polyhedra ⋮ Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques ⋮ Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL ⋮ Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation ⋮ Foundations of dependent interoperability ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ Enabling floating-point arithmetic in the Coq proof assistant ⋮ A Formal Proof of the Computation of Hermite Normal Form in a General Setting ⋮ Flexible Correct-by-Construction Programming ⋮ Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm ⋮ Graph theory in Coq: minors, treewidth, and isomorphisms ⋮ Unnamed Item ⋮ Primitive Floats in Coq ⋮ A formalization of convex polyhedra based on the simplex method ⋮ From Sets to Bits in Coq ⋮ Continuous and monotone machines ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types ⋮ Formally verified certificate checkers for hardest-to-round computation
Uses Software
This page was built for publication: Refinements for Free!
