TE
科技回声
首页24小时热榜最新最佳问答展示工作
GitHubTwitter
首页

科技回声

基于 Next.js 构建的科技新闻平台,提供全球科技新闻和讨论内容。

GitHubTwitter

首页

首页最新最佳问答展示工作

资源链接

HackerNews API原版 HackerNewsNext.js

© 2025 科技回声. 版权所有。

Constructive mathematics and computer programming (1979) [pdf]

130 点作者 mathetic将近 6 年前

5 条评论

AnthonBerg将近 6 年前
Per Martin-Löf writes so beautifully.<p>Here’s more: <a href="https:&#x2F;&#x2F;github.com&#x2F;michaelt&#x2F;martin-lof" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;michaelt&#x2F;martin-lof</a><p>Here’s another one - this one is wonderful: <a href="https:&#x2F;&#x2F;archive-pml.github.io&#x2F;martin-lof&#x2F;pdfs&#x2F;Bibliopolis-Book-retypeset-1984.pdf" rel="nofollow">https:&#x2F;&#x2F;archive-pml.github.io&#x2F;martin-lof&#x2F;pdfs&#x2F;Bibliopolis-Bo...</a><p>As far as I understand the theory, then dependently typed languages such as Idris have their roots in his work on intuitionistic type theory: <a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Intuitionistic_type_theory" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Intuitionistic_type_theory</a><p>Intuitionism in math is beautiful imo: <a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Intuitionism" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Intuitionism</a>
评论 #20426236 未加载
ex3xu将近 6 年前
As a layman I&#x27;m curious about the state of constructivist mathematics and intuitionism since the tragic passing of Vladimir Voevodsky in 2017. I recall reading about the Coq proof assistant, homotopy type theory, and univalent foundations with some interest, but I haven&#x27;t been keeping up with any new developments -- is it still an active field of research?<p>I&#x27;m also curious if someone can weigh in on the fact that this paper by Martin-Löf finishes with a proof of the axiom of choice -- isn&#x27;t that a bit of a controversial axiom? Does all of constructivist mathematics still depend on the axiom of choice to this day?
评论 #20423231 未加载
评论 #20423466 未加载
评论 #20426693 未加载
评论 #20423565 未加载
评论 #20425398 未加载
评论 #20422972 未加载
r00tanon将近 6 年前
Very interesting. Amazing how much we owe, without realizing, to the early pioneers and designers of the first computers, who often prognosticated issues we deal with today.<p>I recently have been researching Leslie Lamport&#x27;s TLA+ project. Definitely in line with the ideas in this paper. <a href="https:&#x2F;&#x2F;lamport.azurewebsites.net&#x2F;tla&#x2F;tla.html" rel="nofollow">https:&#x2F;&#x2F;lamport.azurewebsites.net&#x2F;tla&#x2F;tla.html</a>
评论 #20424837 未加载
codedrome将近 6 年前
Thanks, I&#x27;ll copy this to my tablet so I can carry it around with me.<p>Looking forward to being impressed (hopefully) that it is still relevant today.
评论 #20424591 未加载
ukj将近 6 年前
Few years ago I joined some metaphysical dots between &quot;construction&quot;, &quot;constructivism&quot;, &quot;creation&quot; and &quot;creationism&quot; in my head, which is what led me on to explore 100 years of history&#x2F;theory behind computational trinitarianism, intuitionistic logic, Curry-Howard isomorphism etc.<p>This conceptual understanding of Monist metaphysics was the end of my militant atheism.<p>The expression of knowledge is the creation of knowledge.<p>It pleases me to see that Per Martin-Löf joined the same dots in his paper &quot;A path from logic to metaphysics&quot;.