QPC: QJ-based Proof Compiler - Simple Examples and Analysis
No abstract available.
Related papers
- Code Generation via Meta-programming in Dependently Typed Proof Assistants ESOP 2026
- Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints POPL 1977
- Noninterference through flow analysis JFP 2005
- Oracle-based checking of untrusted software POPL 2001
- LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation CGO 2004
- Monadic refinements for relational cost analysis POPL 2018
- Nominal logic programming TOPLAS 2008
- Completeness and Incompleteness of Trace-Based Network Proof Systems POPL 1987