Fiat
From MaRDI portal
Cited in
(41)- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- 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
- Galculator
- Automatic refinement to efficient data structures: a comparison of two approaches
- VeriML
- KIDS
- From Sets to Bits in Coq
- Proof-based synthesis of sorting algorithms for trees
- Extensible and efficient automation through reflective tactics
- HOL-TestGen
- Verified characteristic formulae for CakeML
- Ssreflect.fintype
- MathComp.tuple
- SyPet
- CodeHint
- JSketch
- DTRE
- CertiCoq
- HALO
- OEuf
- HoTTSQL
- Gallina
- Bedrock
- CAVA Automata Library
- Collections
- Q*cert
- SQLCert
- SEQUEL
- Tree Automata
- Imperative Refinement
- Light-weight Containers
- LTL_to_GBA
- Real_Impl
- Foundations of dependent interoperability
- Constructive Galois connections
- 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
This page was built for software: Fiat
