A Brief Overview of Agda – A Functional Language with Dependent Types (Q3183520): Difference between revisions

@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Dependent Types at Work
@@ Property / cites work: Dependent Types at Work / rank @@
+Normal rank
@@ Property / cites work @@
+The calculus of constructions
@@ Property / cites work: The calculus of constructions / rank @@
+Normal rank
@@ Property / cites work @@
+Inductive families
@@ Property / cites work: Inductive families / rank @@
+Normal rank
@@ Property / cites work @@
+A general formulation of simultaneous inductive-recursive definitions in type theory
+Normal rank
@@ Property / cites work @@
+Indexed induction-recursion
@@ Property / cites work: Indexed induction-recursion / rank @@
+Normal rank
@@ Property / cites work @@
+The Four Colour Theorem: Engineering of a Formal Proof
+Normal rank
@@ Property / cites work @@
+Q3886868
@@ Property / cites work: Q3886868 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3688389
@@ Property / cites work: Q3688389 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999860
@@ Property / cites work: Q3999860 / rank @@
+Normal rank
@@ Property / cites work @@
+Dependently Typed Programming in Agda
@@ Property / cites work: Dependently Typed Programming in Agda / rank @@
+Normal rank