🌘 2025 年阿隆佐·邱奇獎得主
➤ 推值調用演算：邏輯與計算的統一基石
✤ https://siglog.org/winner-of-the-2025-alonzo-church-award/
美國計算機學會（ACM）特殊興趣小組（SIGLOG）宣佈，保羅·布萊恩·列維（Paul Blain Levy）因其對帶有副作用的λ演算的 фундаментальное 研究，特別是透過「推值調用」（Call-by-Push-Value，CBPV）演算的研究，榮獲 2025 年阿隆佐·邱奇獎。他的研究成果將λ演算的純邏輯形式與應用型帶有副作用的形式重新整合，並為計算和邏輯現象的研究提供了一個統一的起點。
+ 「這項獎項非常重要，證明瞭理論計算機科學的貢獻依然受到重視，而且具有深遠影響。」
+ 「推值調用演算聽起來很複雜，但能將不同的研究整合起來，確實令人印象深刻。期待看到這個理論在未來能有更多應用。」
#計算機科學 #邏輯學 #獎項

🌕 命題即類型
➤ 邏輯與計算的深層連結
✤ https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf
本文探討了「命題即類型」原理，闡述了邏輯學與計算機科學之間深刻的關聯。這個原理認為，邏輯中的命題與程式語言中的類型相互對應，命題的證明則對應於程式，簡而言之，命題即類型，證明即程式。該原理源於20世紀30年代的直覺主義邏輯研究，並由多位科學家獨立發展，影響深遠，催生了自動證明輔助工具和多種程式語言。文章追溯了其歷史源流，並探討了其背後深層的哲學和數學意義。
+ 這篇文章讓我意識到數學、邏輯和程式設計之間存在著更深層次的聯繫，以前從未這樣想過！
+ 我對這個原理的歷史發展過程感到非常驚訝，原來這麼多科學家都參與其中，真是令人著迷。
#計算機科學 #邏輯學 #程式語言