Formal polytypic programs and proofs (Q3070767): Difference between revisions

@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Call-by-name, call-by-value and the \(\lambda\)-calculus
+Normal rank
@@ Property / cites work @@
+A UNIVERSE OF STRICTLY POSITIVE FAMILIES
@@ Property / cites work: A UNIVERSE OF STRICTLY POSITIVE FAMILIES / rank @@
+Normal rank
@@ Property / cites work @@
+Type-based termination of generic programs
@@ Property / cites work: Type-based termination of generic programs / rank @@
+Normal rank
@@ Property / cites work @@
+Container types categorically
@@ Property / cites work: Container types categorically / rank @@
+Normal rank
@@ Property / cites work @@
+Derivable Type Classes
@@ Property / cites work: Derivable Type Classes / rank @@
+Normal rank
@@ Property / cites work @@
+Generic programming in 3D
@@ Property / cites work: Generic programming in 3D / rank @@
+Normal rank
@@ Property / cites work @@
+Generics for the masses
@@ Property / cites work: Generics for the masses / rank @@
+Normal rank
@@ Property / cites work @@
+Type checking with universes
@@ Property / cites work: Type checking with universes / rank @@
+Normal rank
@@ Property / cites work @@
+Boxy types
@@ Property / cites work: Boxy types / rank @@
+Normal rank
@@ Property / cites work @@
+Inductive and Coinductive Components of Corecursive Functions in Coq
+Normal rank
@@ Property / cites work @@
+Complete and decidable type inference for GADTs
@@ Property / cites work: Complete and decidable type inference for GADTs / rank @@
+Normal rank