Strongly typed term representations in Coq (Q2392480): Difference between revisions

@@ Property / describes a project that uses @@
+Heq
@@ Property / describes a project that uses: Heq / rank @@
+Normal rank
@@ 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/s10817-011-9219-0
+Normal rank
@@ Property / OpenAlex ID @@
+W1997354605
@@ Property / OpenAlex ID: W1997354605 / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Q4945244
@@ Property / cites work: Q4945244 / rank @@
+Normal rank
@@ Property / cites work @@
+Biorthogonality, step-indexing and compiler correctness
+Normal rank
@@ Property / cites work @@
+Some Domain Theory and Denotational Semantics in Coq
+Normal rank
@@ Property / cites work @@
+de Bruijn notation as a nested datatype
@@ Property / cites work: de Bruijn notation as a nested datatype / rank @@
+Normal rank
@@ Property / cites work @@
+Parametric higher-order abstract syntax for mechanized semantics
+Normal rank
@@ Property / cites work @@
+A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
+Normal rank
@@ Property / cites work @@
+A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
+Normal rank
@@ Property / cites work @@
+Q3994895
@@ Property / cites work: Q3994895 / rank @@
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Nested abstract syntax in Coq
@@ Property / cites work: Nested abstract syntax in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Q4736399
@@ Property / cites work: Q4736399 / rank @@
+Normal rank
@@ Property / cites work @@
+The view from the left
@@ Property / cites work: The view from the left / 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 @@
+Guarded recursive datatype constructors
@@ Property / cites work: Guarded recursive datatype constructors / rank @@
+Normal rank