Types and Programming Languages

• ss5 Untyped Lambda-Calculus

  • web.yl.is.s.u-tokyo.ac.jp/~kohei/rinkou/types/resume/type5.pdf

• ss9 Simply Typed Lambda-Calculus

  • web.yl.is.s.u-tokyo.ac.jp/~kohei/rinkou/types/resume/9.pdf

• ss12 Normalization

  • web.yl.is.s.u-tokyo.ac.jp/~kohei/rinkou/types/resume/12.pdf

• ss13 References

  • web.yl.is.s.u-tokyo.ac.jp/~kohei/rinkou/types/resume/13.pdf

• ss14 Exceptions

• ss15 Subtyping ${\lambda }_{<:}$

  • Structural Subtyping

• ss20 Recursive Types

• ss23 Universal Types

• ss24 Existentioal Types

• ss26 Bounded Quantification

• ss29 Type Operators and Kinding

• ss30 Higher-Order Polymorphism

• https://www.cis.upenn.edu/~bcpierce/attapl/

  • ATTPL(2004): TaPLの続編的な

参考文献

• Rinkou - Types and Programming Languages