Fiat
From MaRDI portal
Software:33165
swMATH21357MaRDI QIDQ33165FDOQ33165
Author name not available (Why is that?)
Cited In (15)
- From Sets to Bits in Coq
- Extensible and Efficient Automation Through Reflective Tactics
- Refinement to imperative HOL
- Fast machine words in Isabelle/HOL
- Proof–Based Synthesis of Sorting Algorithms for Trees
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- Verified Characteristic Formulae for CakeML
- 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)
- Constructive Galois Connections
- 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
- Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
This page was built for software: Fiat
