diff --git a/README.md b/README.md
index ac90e617d7..3f93943d45 100644
--- a/README.md
+++ b/README.md
@@ -45,6 +45,7 @@ Miscellaneous
 - [Git Commit Conventions](doc/commit_convention.md)
 - [Automatic Builds](doc/make/travis.md)
 - [Syntax Highlight Lean Code in LaTeX](doc/syntax_highlight_in_latex.md)
+- [Exporting, and reference type-checkers](doc/export_format.md)
 
 Roadmap
 -------------
diff --git a/doc/export_format.md b/doc/export_format.md
index 89e0792b89..026977765a 100644
--- a/doc/export_format.md
+++ b/doc/export_format.md
@@ -11,6 +11,11 @@ cd lean/library
 lean --export=export.out --recursive
 ```
 
+There are several checkers available that can read these files:
+* [trepplein](https://github.com/gebner/trepplein), a type-checker written in Scala.
+* [tc](https://github.com/dselsam/tc), a type-checker written in Haskell.
+* [leanchecker](https://github.com/leanprover/lean/tree/master/src/checker), a bare-bones version of the Lean kernel.
+
 Hierarchical names
 ------------------