From Sets to Bits in Coq

DOI10.1007/978-3-319-29604-3_2zbMath1475.68455OpenAlexW2230566585MaRDI QIDQ2798253

Pierre-Évariste Dagand, Arthur Blot, Julia L. Lawall

Publication date: 4 April 2016

Published in: Functional and Logic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-29604-3_2

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Coq
• Isabelle/HOL
• Why3
• OCaml
• Fiat
• Ssreflect.fintype
• MathComp.tuple

Cites Work

• Unnamed Item
• Theory and applications of satisfiability testing -- SAT 2008. 11th international conference, SAT 2008, Guangzhou, China, May 12--15, 2008. Proceedings
• Fiat
• A Refinement-Based Approach to Computational Algebra in Coq
• Refinements for Free!
• The B-Book
• A coherence theorem for Martin-Löf's type theory
• Characteristic formulae for the verification of imperative programs
• Data Refinement in Isabelle/HOL
• Space/time trade-offs in hash coding with allowable errors
• A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture

This page was built for publication: From Sets to Bits in Coq