• Practical Foundations for Programming Languages
• Programming Language Foundations in Agda
• Proofs and Types
• Certified Programming with Dependent Types
• Programs and Proofs
• Lectures on the Curry-Howard Isomorphism
• POLYMORPHIC TYPING OF AN ALGORITHMIC LANGUAGE
• Basic Simple Type Theory
• Lambda Calculus and Combinators
• Type Theory and Functional Programming
• Programming in Martin-Lof’s Type Theory
• The HoTT Book | Homotopy Type Theory
• Programming Language Theory
• [1911.00580] Introduction to Univalent Foundations of Mathematics with Agda

意味論

• 計算機科学と代数学 - 計算機科学とは？ 意味論とは？
• プログラミング言語の意味論
• おもしろいみろん - ゲーム意味論

カリー＝ハワード同型対応

型理論と証明論との間の対応。更に圏論との対応まで含めてカリー＝ハワード＝ランベック対応と呼ばれる

• カリー＝ハワード同型対応 - Wikipedia
• Haskell/カリー=ハワード同型
• カリー・ハワード同型対応入門
• Lectures on the Curry-Howard Isomorphism (1998)
• “Program = Proof” by Samuel Mimram (pub. 2020) pdf available online for free. : haskell

集合と論理

• Axiomatic Set Theory
• Set Theory
• Introduction to Axiomatic Set Theory
• 直観主義論理への招待
• The Incredible Proof Machine
• Programs and Proofs
• Notes on Proof Theory: Part 1
• Programs as proofs
• Proof Theory Foundations, Lecture 1, 2, 3, 4
• Computability
• Relational Methods in Computer Science
• Second-order theories should not be taken lightly
• Some reasons to teach lattice theory to undergraduates
• 代数的視点からの論理へのアプローチ
• 東京大学数理科学研究科「数学基礎論・数理科学続論D」の講義資料
• Understanding Constructive Galois Connections
• Classical Logic in Haskell - SAOWEN
• Cantor Pairing
• [2002.00188] Intuitionistic Fixed Point Logic
• [2101.11320] Tutorial on implementing Hoare logic for imperative programs in Haskell