N. G. de Bruijn's contribution to the formalization of mathematics (Q740481): Difference between revisions

@@ Property / DOI @@
-.1016/j.indag.2013.09.003
@@ Property / DOI: 10.1016/j.indag.2013.09.003 / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+NQTHM
@@ Property / describes a project that uses: NQTHM / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ML
@@ Property / describes a project that uses: ML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Twelf
@@ Property / describes a project that uses: Twelf / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LCF
@@ Property / describes a project that uses: LCF / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SAD
@@ Property / describes a project that uses: SAD / 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 @@
+Automath
@@ Property / describes a project that uses: Automath / 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.1016/j.indag.2013.09.003
+Normal rank
@@ Property / OpenAlex ID @@
+W2151993589
@@ Property / OpenAlex ID: W2151993589 / rank @@
+Normal rank
@@ Property / cites work @@
+Explicit substitutions
@@ Property / cites work: Explicit substitutions / rank @@
+Normal rank
@@ Property / cites work @@
+The lambda calculus. Its syntax and semantics. Rev. ed.
+Normal rank
@@ Property / cites work @@
+Q4023900
@@ Property / cites work: Q4023900 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751370
@@ Property / cites work: Q2751370 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4040283
@@ Property / cites work: Q4040283 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5565113
@@ Property / cites work: Q5565113 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5667469
@@ Property / cites work: Q5667469 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4175528
@@ Property / cites work: Q4175528 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4012875
@@ Property / cites work: Q4012875 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4247300
@@ Property / cites work: Q4247300 / rank @@
+Normal rank
@@ Property / cites work @@
+N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker
+Normal rank
@@ Property / cites work @@
+Q2878128
@@ Property / cites work: Q2878128 / rank @@
+Normal rank
@@ Property / cites work @@
+Simple Types in Type Theory: Deep and Shallow Encodings
+Normal rank
@@ Property / cites work @@
+Q4513619
@@ Property / cites work: Q4513619 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+Q3618853
@@ Property / cites work: Q3618853 / rank @@
+Normal rank
@@ Property / cites work @@
+Explicit substitutions with de bruijn's levels
@@ Property / cites work: Explicit substitutions with de bruijn's levels / rank @@
+Normal rank
@@ Property / cites work @@
+Q4296744
@@ Property / cites work: Q4296744 / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+Q3688389
@@ Property / cites work: Q3688389 / rank @@
+Normal rank
@@ Property / cites work @@
+Recursive functions of symbolic expressions and their computation by machine, Part I
+Normal rank
@@ Property / cites work @@
+Q5519616
@@ Property / cites work: Q5519616 / rank @@
+Normal rank
@@ Property / cites work @@
+Type Theory and Formal Proof
@@ Property / cites work: Type Theory and Formal Proof / rank @@
+Normal rank
@@ Property / cites work @@
+Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
+Normal rank
@@ Property / cites work @@
+Q3999860
@@ Property / cites work: Q3999860 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5606586
@@ Property / cites work: Q5606586 / rank @@
+Normal rank
@@ Property / cites work @@
+A type-theoretical alternative to ISWIM, CUCH, OWHY
+Normal rank
@@ Property / cites work @@
+Q5533180
@@ Property / cites work: Q5533180 / rank @@
+Normal rank
@@ Property / cites work @@
+Intensional interpretations of functionals of finite type I
+Normal rank
@@ Property / cites work @@
+Interacting with Modal Logics in the Coq Proof Assistant
+Normal rank
@@ Property / cites work @@
+Q4187337
@@ Property / cites work: Q4187337 / rank @@
+Normal rank
@@ Property / cites work @@
+On Correctness of Mathematical Texts from a Logical and Practical Point of View
+Normal rank
@@ Property / cites work @@
+The Isabelle Framework
@@ Property / cites work: The Isabelle Framework / rank @@
+Normal rank
@@ Property / cites work @@
+A new implementation of Automath
@@ Property / cites work: A new implementation of Automath / rank @@
+Normal rank
@@ Property / DOI @@
+.1016/J.INDAG.2013.09.003
@@ Property / DOI: 10.1016/J.INDAG.2013.09.003 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:740481