Program development in constructive type theory (Q1190474): Difference between revisions

@@ Property / describes a project that uses @@
+Automath
@@ Property / describes a project that uses: Automath / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nuprl
@@ Property / describes a project that uses: Nuprl / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+The calculus of constructions
@@ Property / cites work: The calculus of constructions / rank @@
+Normal rank
@@ Property / cites work @@
+A synthesis of several sorting algorithms
@@ Property / cites work: A synthesis of several sorting algorithms / rank @@
+Normal rank
@@ Property / cites work @@
+Q3685173
@@ Property / cites work: Q3685173 / rank @@
+Normal rank
@@ Property / cites work @@
+The system \({\mathcal F}\) of variable types, fifteen years later
+Normal rank
@@ Property / cites work @@
+Q3478405
@@ Property / cites work: Q3478405 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3477935
@@ Property / cites work: Q3477935 / rank @@
+Normal rank
@@ Property / cites work @@
+Constructive mathematics and computer programming
@@ Property / cites work: Constructive mathematics and computer programming / rank @@
+Normal rank
@@ Property / cites work @@
+Terminating general recursion
@@ Property / cites work: Terminating general recursion / rank @@
+Normal rank
@@ Property / cites work @@
+Constructing recursion operators in intuitionistic type theory
+Normal rank
@@ Property / cites work @@
+The foundation of a generic theorem prover
@@ Property / cites work: The foundation of a generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+A set constructor for inductive sets in Martin-Löf's type theory
+Normal rank
@@ Property / cites work @@
+Q3673095
@@ Property / cites work: Q3673095 / rank @@
+Normal rank