The following pages link to Adam Chlipala (Q1702890):
Displaying 22 items.
- Modular deductive verification of multiprocessor hardware designs (Q1702892) (← links)
- Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms (Q1722642) (← links)
- Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac} (Q1791170) (← links)
- Fiat (Q2819861) (← links)
- Chapar: certified causally consistent distributed key-value stores (Q2828279) (← links)
- Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms (Q2829257) (← links)
- Experience Implementing a Performant Category-Theory Library in Coq (Q2879258) (← links)
- Compositional Computational Reflection (Q2879264) (← links)
- Effective interactive proofs for higher-order imperative programs (Q2936804) (← links)
- (Q3075245) (← links)
- Modular development of certified program verifiers with a proof assistant, (Q3546045) (← links)
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs (Q5048997) (← links)
- Computable decision making on the reals and other spaces (Q5145365) (← links)
- Parametric higher-order abstract syntax for mechanized semantics (Q5178760) (← links)
- A verified compiler for an impure functional language (Q5255065) (← links)
- A program optimization for automatic database result caching (Q5370861) (← links)
- (Q5417200) (← links)
- Static Analysis (Q5466565) (← links)
- Verification, Model Checking, and Abstract Interpretation (Q5898617) (← links)
- Accelerating verified-compiler development with a verified rewriting engine (Q6572554) (← links)
- Automatic test-case reduction in proof assistants: a case study in Coq (Q6572555) (← links)
- Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq (Q6611970) (← links)
