Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
We address the challenges of scaling verification efforts to match the increasing complexity and size of systems. We propose a research agenda aimed at building a performant proof engine by studying the asymptotic performance of proof engines and redesigning their building blocks. As a case study, w...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Springer Netherlands
2024
|
| Online Access: | https://hdl.handle.net/1721.1/156261 |