Algebra of programming in Agda: Dependent types for relational program derivation (Q3644935): Difference between revisions

@@ Property / describes a project that uses @@
+ALF
@@ Property / describes a project that uses: ALF / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+AoPA
@@ Property / describes a project that uses: AoPA / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Cayenne
@@ Property / describes a project that uses: Cayenne / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Agda
@@ Property / describes a project that uses: Agda / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q114849894
@@ Property / Wikidata QID: Q114849894 / rank @@
+Normal rank
@@ Property / cites work @@
+Cayenne—a language with dependent types
@@ Property / cites work: Cayenne—a language with dependent types / 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 @@
+Type checking with universes
@@ Property / cites work: Type checking with universes / rank @@
+Normal rank
@@ Property / cites work @@
+Eliminating Dependent Pattern Matching
@@ Property / cites work: Eliminating Dependent Pattern Matching / rank @@
+Normal rank
@@ Property / cites work @@
+Inductive families
@@ Property / cites work: Inductive families / rank @@
+Normal rank
@@ Property / cites work @@
+Reductivity
@@ Property / cites work: Reductivity / rank @@
+Normal rank
@@ Property / cites work @@
+Dependent ML An approach to practical programming with dependent types
+Normal rank
@@ Property / cites work @@
+Deforestation: Transforming programs to eliminate trees
+Normal rank
@@ Property / cites work @@
+Proving Properties of Programs by Structural Induction
+Normal rank
@@ Property / cites work @@
+A lattice-theoretical fixpoint theorem and its applications
+Normal rank
@@ Property / cites work @@
+Modelling general recursion in type theory
@@ Property / cites work: Modelling general recursion in type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Terminating general recursion
@@ Property / cites work: Terminating general recursion / rank @@
+Normal rank
@@ Property / cites work @@
+Functional algorithm design
@@ Property / cites work: Functional algorithm design / rank @@
+Normal rank
@@ Property / cites work @@
+Algebra of Programming Using Dependent Types
@@ Property / cites work: Algebra of Programming Using Dependent Types / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and applications of inverting functions as folds
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:3644935