Andy Melnikov (nponeccop) wrote,
Andy Melnikov

A Modern Perspective on Type Theory: From its Origins until Today

К сожалению, даже украденной нету :(

Review: A Modern Perspective on Type Theory: From its Origins until Today, by Fairouz Kamareddine, Twan Laan, and Rob Nederpelt

This brief description — largely borrowed from the book under review — shows an exciting evolution and convergence of ideas related to type theory. While many logicians seem to be aware of this story, many researchers are still only familiar with one side of it. For example, specialists in foundations of set theory are quite familiar with Russell’s type theory, and may be aware of intuitionistic mathematics, but they may not know much about the relation between intutionistic (constructive) logic and type theory. Specialists in theoretical computer science are usually quite familiar with recursive functions and λ-calculus, but
not with set-theoretical types and the use of PAT in proof checking. Specialists in programming languages may be familiar with types and type checking, but are usually not aware of the relation between these (practical) types and more theoretical work that they may have studied in Theory of Computations and AI classes. Specialists in AI are usually familiar with LISP—and maybe with proof checking software, but they are usually not aware of the deep relation between the two and of the relation between these subjects and foundations of set theory.

One reason why the relationship is not well known is that up to know, different aspects of type theory were presented in different forms, sometimes informally. The authors meticulously go over the past formalisms and approaches and describe them in a similar way, so that modern readers will be able to understand all the details of each formalism — and the relation between different type theories and between their various applications.

The result is a very useful book

  • Post a new comment


    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.