Fiat
From MaRDI portal
Software:33165
No author found.
Related Items (15)
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers ⋮ Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs ⋮ Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques ⋮ Foundations of dependent interoperability ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ Verified Characteristic Formulae for CakeML ⋮ Refinement to imperative HOL ⋮ A Coq formalisation of SQL's execution engines ⋮ Software verification with ITPs should use binary code extraction to reduce the TCB (short paper) ⋮ Fast machine words in Isabelle/HOL ⋮ Relational parametricity and quotient preservation for modular (co)datatypes ⋮ From Sets to Bits in Coq ⋮ Proof–Based Synthesis of Sorting Algorithms for Trees ⋮ Extensible and Efficient Automation Through Reflective Tactics ⋮ Constructive Galois Connections
This page was built for software: Fiat
