A Mechanically Verified Application for a Mechanically Verified Environment
No abstract available.
Related papers
- Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language ICFP 2025
- Mechanizing conventional SSA for a verified destruction with coalescing CC 2016
- Developing and certifying Datalog optimizations in coq/mathcomp CPP 2021
- Aloe: verifying reliability of approximate programs in the presence of recovery mechanisms CGO 2020
- Leto: verifying application-specific hardware fault tolerance with programmable execution models OOPSLA 2018
- Mechanized semantics and verified compilation for a dataflow synchronous language with reset POPL 2020
- Meta-level features in an industrial-strength theorem prover POPL 2012
- Mechanically Verifying a Family of Multiplier Circuits CAV 1996