diff --git a/docs/Compilation/AutoInitialization.md b/docs/Compilation/AutoInitialization.md
index 6c6b69dbf58..48eaabf3e41 100644
--- a/docs/Compilation/AutoInitialization.md
+++ b/docs/Compilation/AutoInitialization.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Automatic Initialization of Variables
+---
 
 Automatic Initialization of Variables
 =====================================
diff --git a/docs/Compilation/Boogie.md b/docs/Compilation/Boogie.md
index 2ba8d85debe..b219dba84e2 100644
--- a/docs/Compilation/Boogie.md
+++ b/docs/Compilation/Boogie.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Dafny compilation to Boogie
+---
 
 # Dafny compilation to Boogie
 
diff --git a/docs/Compilation/Go.md b/docs/Compilation/Go.md
index 0df9c7a0c87..5b254c1353b 100644
--- a/docs/Compilation/Go.md
+++ b/docs/Compilation/Go.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Dafny compilation to Go
+---
 
 Dafny compilation to Go
 =======================
diff --git a/docs/Compilation/ReferenceTypes.md b/docs/Compilation/ReferenceTypes.md
index d085facb7a7..ee15aa31841 100644
--- a/docs/Compilation/ReferenceTypes.md
+++ b/docs/Compilation/ReferenceTypes.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Dafny compilation of trait and class
+---
 
 Dafny compilation of trait and class
 ====================================
diff --git a/docs/Compilation/StringsAndChars.md b/docs/Compilation/StringsAndChars.md
index be404658f2a..30b671f5679 100644
--- a/docs/Compilation/StringsAndChars.md
+++ b/docs/Compilation/StringsAndChars.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Strings and Characters
+---
 
 # Strings and Characters
 
diff --git a/docs/HowToFAQ/FAQForallTricks.md b/docs/HowToFAQ/FAQForallTricks.md
index 76cb5e48404..e9aca723f5a 100644
--- a/docs/HowToFAQ/FAQForallTricks.md
+++ b/docs/HowToFAQ/FAQForallTricks.md
@@ -1,10 +1,10 @@
 ---
-title: Why can't I write 'forall t: Test :: t.i == 1' for an object t?
+title: "Why can't I write `forall t: Test :: t.i == 1` for an object `t`?"
 ---
 
 ## Question:
 
-Why can't I write `forall t: Test :: t.i == 1` for an object t?
+Why can\'t I write `forall t: Test :: t.i == 1` for an object `t`?
 
 ## Answer:
 
diff --git a/docs/Installation.md b/docs/Installation.md
index d52c7898093..897e5b5923a 100644
--- a/docs/Installation.md
+++ b/docs/Installation.md
@@ -239,7 +239,7 @@ To setup Dafny to compile to python3:
 
 To separately compile and run your program for Python:
 - `dafny build -t:py MyProgram.dfy`
-- `python3 MyProgram-py/MyProgram.py
+- `python3 MyProgram-py/MyProgram.py`
 
 ### Rust
 
diff --git a/docs/OnlineTutorial/Lemmas.md b/docs/OnlineTutorial/Lemmas.md
index f2fa5a5e651..48bda036d71 100644
--- a/docs/OnlineTutorial/Lemmas.md
+++ b/docs/OnlineTutorial/Lemmas.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Lemmas and Induction
+---
 
 # Lemmas and Induction
 
diff --git a/docs/OnlineTutorial/Modules.md b/docs/OnlineTutorial/Modules.md
index d5add36f5b8..15c56d3e5f5 100644
--- a/docs/OnlineTutorial/Modules.md
+++ b/docs/OnlineTutorial/Modules.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Modules
+---
 
 # Modules
 
diff --git a/docs/OnlineTutorial/Sequences.md b/docs/OnlineTutorial/Sequences.md
index 79347d4b457..78c6480143c 100644
--- a/docs/OnlineTutorial/Sequences.md
+++ b/docs/OnlineTutorial/Sequences.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Sequences
+---
 
 # Sequences
 
diff --git a/docs/OnlineTutorial/Sets.md b/docs/OnlineTutorial/Sets.md
index fa363f9eded..0b01c7cf0bc 100644
--- a/docs/OnlineTutorial/Sets.md
+++ b/docs/OnlineTutorial/Sets.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Sets
+---
 
 # Sets
 
diff --git a/docs/OnlineTutorial/Termination.md b/docs/OnlineTutorial/Termination.md
index a3254cd7b4a..68a5d1bb157 100644
--- a/docs/OnlineTutorial/Termination.md
+++ b/docs/OnlineTutorial/Termination.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Termination
+---
 
 # Termination
 
diff --git a/docs/OnlineTutorial/ValueTypes.md b/docs/OnlineTutorial/ValueTypes.md
index a938fde171e..b42442360c2 100644
--- a/docs/OnlineTutorial/ValueTypes.md
+++ b/docs/OnlineTutorial/ValueTypes.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: Collection Types
+---
 
 # Collection Types
 
diff --git a/docs/OnlineTutorial/guide.md b/docs/OnlineTutorial/guide.md
index 753d6ec1fc7..baa3c5e3329 100644
--- a/docs/OnlineTutorial/guide.md
+++ b/docs/OnlineTutorial/guide.md
@@ -1,4 +1,6 @@
-<p></p> <!-- avoids duplicate title -->
+---
+title: "Getting Started with Dafny: A Guide"
+---
 
 # Getting Started with Dafny: A Guide
 
diff --git a/docs/QuickReference.md b/docs/QuickReference.md
index 4dfef1d4579..b3e92be4bc2 100755
--- a/docs/QuickReference.md
+++ b/docs/QuickReference.md
@@ -1,5 +1,6 @@
-<p></p>
-<link rel="stylesheet" href="assets/main.css">
+---
+title: Dafny Quick Reference
+---
 
 # Dafny Quick Reference
 
diff --git a/docs/_config.yml b/docs/_config.yml
index 9a0e827a943..57af79d8795 100644
--- a/docs/_config.yml
+++ b/docs/_config.yml
@@ -65,3 +65,11 @@ exclude:
    - vendor/cache/
    - vendor/gems/
    - vendor/ruby/
+   - "*.expect"
+
+defaults:
+  -
+    scope:
+      path: "" # an empty string here means all files in the project
+    values:
+      layout: "single"
\ No newline at end of file
diff --git a/docs/_layouts/single.html b/docs/_layouts/single.html
new file mode 100644
index 00000000000..32800307467
--- /dev/null
+++ b/docs/_layouts/single.html
@@ -0,0 +1,18 @@
+<!DOCTYPE html>
+<html lang="{{ page.lang | default: site.lang | default: "en" }}">
+
+{%- include head.html -%}
+
+<body>
+
+  <main class="page-content" aria-label="Content">
+    <div class="wrapper">
+      {{ content }}
+    </div>
+  </main>
+
+  {%- include footer.html -%}
+
+</body>
+
+</html>