Extensible and Efficient Automation Through Reflective Tactics (Q2802496): Difference between revisions

@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-662-49498-1_21
+Normal rank
@@ Property / OpenAlex ID @@
+W2478126725
@@ Property / OpenAlex ID: W2478126725 / rank @@
+Normal rank
@@ Property / cites work @@
+Program Logics for Certified Compilers
@@ Property / cites work: Program Logics for Certified Compilers / rank @@
+Normal rank
@@ Property / cites work @@
+A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
+Normal rank
@@ Property / cites work @@
+Q3075242
@@ Property / cites work: Q3075242 / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq
+Normal rank
@@ Property / cites work @@
+Charge!
@@ Property / cites work: Charge! / rank @@
+Normal rank
@@ Property / cites work @@
+Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
+Normal rank
@@ Property / cites work @@
+Modular SMT Proofs for Fast Reflexive Checking Inside Coq
+Normal rank
@@ Property / cites work @@
+Tactics for Reasoning Modulo AC in Coq
@@ Property / cites work: Tactics for Reasoning Modulo AC in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Type Theory Should Eat Itself
@@ Property / cites work: Type Theory Should Eat Itself / rank @@
+Normal rank
@@ Property / cites work @@
+Modular development of certified program verifiers with a proof assistant,
+Normal rank
@@ Property / cites work @@
+Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation
+Normal rank
@@ Property / cites work @@
+A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
+Normal rank
@@ Property / cites work @@
+Fiat
@@ Property / cites work: Fiat / rank @@
+Normal rank
@@ Property / cites work @@
+Typed syntactic meta-programming
@@ Property / cites work: Typed syntactic meta-programming / rank @@
+Normal rank
@@ Property / cites work @@
+Proof-Producing Reflection for HOL
@@ Property / cites work: Proof-Producing Reflection for HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Simple Types in Type Theory: Deep and Shallow Encodings
+Normal rank
@@ Property / cites work @@
+How to make ad hoc proof automation less ad hoc
@@ Property / cites work: How to make ad hoc proof automation less ad hoc / rank @@
+Normal rank
@@ Property / cites work @@
+A compiled implementation of strong reduction
@@ Property / cites work: A compiled implementation of strong reduction / rank @@
+Normal rank
@@ Property / cites work @@
+Importing HOL Light into Coq
@@ Property / cites work: Importing HOL Light into Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Auto in Agda
@@ Property / cites work: Auto in Agda / rank @@
+Normal rank
@@ Property / cites work @@
+Formal certification of a compiler back-end or
@@ Property / cites work: Formal certification of a compiler back-end or / rank @@
+Normal rank
@@ Property / cites work @@
+Compositional Computational Reflection
@@ Property / cites work: Compositional Computational Reflection / rank @@
+Normal rank
@@ Property / cites work @@
+Toward a verified relational database management system
+Normal rank
@@ Property / cites work @@
+VeriML
@@ Property / cites work: VeriML / rank @@
+Normal rank
@@ Property / cites work @@
+Q4364399
@@ Property / cites work: Q4364399 / rank @@
+Normal rank
@@ Property / cites work @@
+Mtac
@@ Property / cites work: Mtac / rank @@
+Normal rank