The \textsc{MetaCoq} project (Q2209542): Difference between revisions

@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-019-09540-0
+Normal rank
@@ Property / OpenAlex ID @@
+W2953833525
@@ Property / OpenAlex ID: W2953833525 / rank @@
+Normal rank
@@ Property / cites work @@
+Type theory in type theory using quotient inductive types
+Normal rank
@@ Property / cites work @@
+Towards certified meta-programming with typed Template-Coq
+Normal rank
@@ Property / cites work @@
+Extending Coq with Imperative Features and Its Application to SAT Verification
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9--12, 2018. Proceedings
+Normal rank
@@ Property / cites work @@
+Proofs for free
@@ Property / cites work: Proofs for free / rank @@
+Normal rank
@@ Property / cites work @@
+HOL Light QE
@@ Property / cites work: HOL Light QE / 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 @@
+Elaborator reflection: extending Idris in Idris
@@ Property / cites work: Elaborator reflection: extending Idris in Idris / rank @@
+Normal rank
@@ Property / cites work @@
+Q3651735
@@ Property / cites work: Q3651735 / rank @@
+Normal rank
@@ Property / cites work @@
+Typed syntactic meta-programming
@@ Property / cites work: Typed syntactic meta-programming / rank @@
+Normal rank
@@ Property / cites work @@
+Q4663833
@@ Property / cites work: Q4663833 / rank @@
+Normal rank
@@ Property / cites work @@
+A certifying extraction with time bounds from Coq to call-by-value
  $\lambda$-calculus
+Normal rank
@@ Property / cites work @@
+Weak call-by-value lambda calculus as a model of computation in Coq
+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 @@
+Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac}
+Normal rank
@@ Property / cites work @@
+The Definitional Side of the Forcing
@@ Property / cites work: The Definitional Side of the Forcing / rank @@
+Normal rank
@@ Property / cites work @@
+Programming in the λ-Calculus: From Church to Scott and Back
+Normal rank
@@ Property / cites work @@
+Q4649560
@@ Property / cites work: Q4649560 / rank @@
+Normal rank
@@ Property / cites work @@
+Canonicity of weak \(\omega\)-groupoid laws using parametricity theory
+Normal rank
@@ Property / cites work @@
+Extensible and Efficient Automation Through Reflective Tactics
+Normal rank
@@ Property / cites work @@
+Efficient self-interpretation in lambda calculus
@@ Property / cites work: Efficient self-interpretation in lambda calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Program-ing finger trees in C             <scp>oq</scp>
@@ Property / cites work: Program-ing finger trees in C <scp>oq</scp> / rank @@
+Normal rank
@@ Property / cites work @@
+MetaML and multi-stage programming with explicit annotations
+Normal rank
@@ Property / cites work @@
+A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
+Normal rank
@@ Property / cites work @@
+Mtac: A monad for typed tactic programming in Coq
@@ Property / cites work: Mtac: A monad for typed tactic programming in Coq / rank @@
+Normal rank