Dependent Types at Work (Q5191088): Difference between revisions

@@ Property / describes a project that uses @@
+Agda
@@ Property / describes a project that uses: Agda / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Polyp
@@ Property / describes a project that uses: Polyp / 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 @@
+Haskell
@@ Property / describes a project that uses: Haskell / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nuprl
@@ Property / describes a project that uses: Nuprl / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Epigram
@@ Property / describes a project that uses: Epigram / 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/978-3-642-03153-3_2
+Normal rank
@@ Property / OpenAlex ID @@
+W1511530761
@@ Property / OpenAlex ID: W1511530761 / rank @@
+Normal rank
@@ Property / cites work @@
+On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
+Normal rank
@@ Property / cites work @@
+Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
+Normal rank
@@ 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 @@
+Modelling general recursion in type theory
@@ Property / cites work: Modelling general recursion in type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q4012882
@@ Property / cites work: Q4012882 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3400627
@@ Property / cites work: Q3400627 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4012883
@@ Property / cites work: Q4012883 / 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 @@
+Q4263867
@@ Property / cites work: Q4263867 / rank @@
+Normal rank
@@ Property / cites work @@
+Indexed induction-recursion
@@ Property / cites work: Indexed induction-recursion / rank @@
+Normal rank
@@ Property / cites work @@
+A new approach to generic functional programming
@@ Property / cites work: A new approach to generic functional programming / rank @@
+Normal rank
@@ Property / cites work @@
+Q5638283
@@ Property / cites work: Q5638283 / rank @@
+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 @@
+Advanced Functional Programming
@@ Property / cites work: Advanced Functional Programming / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999860
@@ Property / cites work: Q3999860 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4414308
@@ Property / cites work: Q4414308 / rank @@
+Normal rank
@@ Property / cites work @@
+LCF considered as a programming language
@@ Property / cites work: LCF considered as a programming language / rank @@
+Normal rank
@@ Property / cites work @@
+MetaML and multi-stage programming with explicit annotations
+Normal rank
@@ Property / cites work @@
+Q4003339
@@ Property / cites work: Q4003339 / rank @@
+Normal rank