Treatise on intuitionistic type theory (Q639262)

This book, extracted from the author's PhD thesis, is a presentation of Martin-Löf intuitionistic type theory. It is based on several contributions by Martin-Löf that were presented only in the form of lectures, but there are also new technical contributions, such as the addition of coinductive definitions and use of eager evaluation, instead of lazy evaluation. The result combines philosophy, mathematical logic and computer science.