Cited in
(41)- 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
- Galculator
- VeriML
- KIDS
- HOL-TestGen
- HALO
- CodeHint
- MathComp.tuple
- JSketch
- Ssreflect.fintype
- CertiCoq
- DTRE
- SyPet
- HoTTSQL
- Gallina
- OEuf
- Bedrock
- CAVA Automata Library
- Collections
- Q*cert
- SEQUEL
- Imperative Refinement
- Light-weight Containers
- LTL_to_GBA
- Real_Impl
- SQLCert
- Tree Automata
- 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
- Automatic refinement to efficient data structures: a comparison of two approaches
- Foundations of dependent interoperability
- Extensible and efficient automation through reflective tactics
This page was built for software: Fiat
