Fiat

swMATH21357MaRDI QIDQ33165FDOQ33165

Author name not available (Why is that?)

Described by source

• Fiat: deductive synthesis of abstract data types in a proof assistant

Cited In (15)

• From Sets to Bits in Coq
• Constructive Galois connections
• Refinement to imperative HOL
• Verified characteristic formulae for CakeML
• Fast machine words in Isabelle/HOL
• Concise read-only specifications for better synthesis of programs with pointers
• Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
• Proof-based synthesis of sorting algorithms for trees
• A Coq formalisation of SQL's execution engines
• Relational parametricity and quotient preservation for modular (co)datatypes
• Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
• Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
• Foundations of dependent interoperability
• Automatic refinement to efficient data structures: a comparison of two approaches
• Extensible and efficient automation through reflective tactics

This page was built for software: Fiat