Directory of Martin-Löf's Type Theory Resources

Home > Science > Math > Logic and Foundations > Nonstandard Logics and Extensions > Intuitionistic Logic > Martin-Löf's Type Theory

Resources in This Category

• Extensional Concepts in Intensional Type Theory

  http://www.dcs.ed.ac.uk/lfcsreps/EXPORT/95/ECS-LFCS-95-327/index.html
  PhD thesis of Martin Hofmann, which shows how the intensional, constructive view of equality in Martin-Löf's Type Theory can be reconciled with the classical, extensional view of identity.

• Implementing Mathematics Using NuPrl

  http://www.cs.cornell.edu/Info/Projects/NuPrl/book/doc.html
  Full online text of the book. Includes tutorial on Martin-Löf's type theory, motivating remarks on intuitionism, as well as sample formalisations of constructive mathematics in the NuPrl theorem prover.

• Martin-Löf Type Theory: Semantics and Proof Theory

  http://www.cs.chalmers.se/~coquand/Sem.html
  Home page of a working group maintained by Thierry Coquand.

• Nuprl Project Related Web Sites

  http://www.cs.cornell.edu/Info/Projects/NuPrl/html/publication.html
  NuPRL is the oldest theorem prover based on Martin-Löf's Type Theory.

 

Home > Science > Math > Logic and Foundations > Nonstandard Logics and Extensions > Intuitionistic Logic > Martin-Löf's Type Theory

 

---

 

Thanks to DMOZ, which built a great web directory for nearly two decades and freely shared it with the web. About us