- 型システム入門 −プログラミング言語と型の理論
- From Type Theory to Haskell in 10 Minutes
- THE TYPE THEORY PODCAST
- Making Sense of Subtypes
- Propositions as Types
- Certified Programming with Dependent Types
- ＭＬの光と影
- 数学基礎論特論 (コンピュータ特別講義 I) 講師 龍田 真
- PROOFS AND TYPES
- Types and Programming Languages
- The Girard-Reynolds isomorphism
- Type Theory and Functional Programming
- Advanced Topics in Types and Programming Languages
- Isomorphisms as equalities
- Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
- Categorical Programming for Data Types with Restricted Parametricity
- Two Different Flavors of Type Theory
- Generic Evaluators
- Several types of types in programming languages
- Strange Loop: “Propositions as Types” by Philip Wadler
- Gabriel439/Haskell-Morte-Library
- type-theory/type-theory-study-group-2015
- 型推論を実装してみる
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Interactive Theorem Proving with Lean
- “Propositions as Types” by Philip Wadler
- Extensional Constructs in Intensional Type Theory
- Semantics of Type Theory
- An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof
- History and Philosophy of Constructive Type Theory
- Types for Proofs and Programs
- Proving With Types
- Monadic regions
- Bidirectional Typing Rules: A Tutorial
- [型理論I (<特集>関数型プログラミングと計算の基礎)](http://ci.nii.ac.jp/naid/110003743606/)
- 型理論II
- 型理論III
- 型理論IV
- variable-free type theoryの圏論的な解釈について
- Cubical Higher Type Theory as a Programming Language
- Hindley-Milner Inference
- Hindley-Damas-Milner tutorial
- Haskell for all: The Curry-Howard correspondence between programs and proofs
- One Eilenberg Theorem to Rule Them All - YouTube
- Algebraic Subtyping
- Haskellの型と直観論理 - 朝日ネット 技術者ブログ
- https://mobile.twitter.com/metaphusika/status/1189909829487251456
- Synthetic topology of data types and classical spaces
- https://twitter.com/masahiro_sakai/status/1181049298932224001
- Free Theorems!
Martin-L¨of ’s Type Theory
- 1972 - An intuitionistic theory of types
- 1979 - Constructive mathematics and computer programming
- 1984 - Intuitionistic Type Theory
- Programming in Martin-L¨of ’s Type Theory
Dependent Type Theory
- Robert Harper - Type Theory Foundations 1 2 3 4 5 6
- ΠΣ: Dependent Types without the Sugar
- 2015 Introduction to Dependent Type Theory — Robert Harper (OPLSS ‘15)
- Dependent Type Theory (Part 1 of 6 ). The Logical Interpretation.
- A Tutorial Implementation of a Dependently Typed Lambda Calculus
- Syntax and Semantics of Dependent Types
- Games for Dependent Types
- 06 Dependent Types Effects and Efficient Verification Conditions in F star
- Designing Dependently-Typed Programming Languages - Lecture 1 - Stephanie Weirich
- Dependent Types for Low-Level Programming
- Unified Interpreters For Dependent Languages
- Guarded Dependent Type Theory with Coinductive Types
- Type Soundness for Path Polymorphism
- Dependent Type in Haskell: Theory And Practice
- The meta-theory of dependent type theories - Vladimir Voevodsky - YouTube
Homotopy Type Theory
ここ数年における新しい理論「ホモトピー型理論(HoTT)」は, 計算機科学の型理論における「＝」を, 位相幾何学のホモトピー同値「連続変形がある」の性質で解釈しようとする試みである。
出典: http://phsc.jp/dat/rsm/2013_a3-1.pdf
- Introduction to Homotopy Type Theory
- TYPE THEORY AND HOMOTOPY
- The HoTT Book
- Lambda Jam 2014 - Gershom Bazerman - Homotopy Type Theory: What’s the Big Idea
- Homotopy before type theory
HoTT is a constructive, proof-relevant theory of equality inside dependent type theory
出典: ICFP 2014: session “Homotopy Type Theory”
- inductive type
- higher inductive type
- Higher Inductive Types: a tour of the menagerie
- Homotopical Patch Theory
- Dan Licata, Guillaume Brunerie, and Peter Lumsdaine, Homotopy Theory in Type Theory
- Univalence as a New Principle of Logic
- 15-819 Homotopy Type Theory
- Homotopy Type Theory project
- ∞カテゴリー
- ∞カテゴリーII
- ∞カテゴリーIII
- ∞カテゴリーIV
- Univalent universes for elegant models of homotopy types
- Does Homotopy Type Theory Provide a Foundation for Mathematics?
- A survey of Univalent Foundations (by Eric Finster, November 13th, 2014)
- Type Theory in Type Theory using Quotient Inductive Types
- Type Theory through Comprehension Categories
- Dependent Inductive and Coinductive Types are Fibrational Dialgebras
- Homotopy Type Theory DMV2015
- The encode-decode method in HoTT, relationally
- The equivalence of the torus and the product of two circles in homotopy type theory
- Categorical homotopy theory
- Constructing the Propositional Truncation using Non-recursive HITs
- Categories, Bundles and Spacetime Topology
- Colimits in HoTT
- 3 01 A Functional Programmer’s Guide to Homotopy Type Theory
- Containers in Homotopy Type Theory