diff --git a/README.md b/README.md index bed6f4c..cca1687 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,6 @@ -# MartinLoefTheorem-Dissertation -Formalising Martin Loef's Theorem Using Coq - Honours Dissertation +# Formalising Martin-Löf's Theorem Using Coq +By Daniel Britten - supervised by Cristian S. Calude - and with guidance from Monica Marcus. + +Source code for an honours dissertation at the University of Auckland. + +In order to interactively step through the proofs in this dissertation, CoqIde can be downloaded from https://coq.inria.fr/download.