diff --git a/.github/workflows/Docs.yml b/.github/workflows/Docs.yml
new file mode 100644
index 0000000..73ee754
--- /dev/null
+++ b/.github/workflows/Docs.yml
@@ -0,0 +1,38 @@
+name: Documentation
+
+on:
+  push:
+    branches:
+      - main
+    tags: '*'
+  pull_request:
+    branches:
+      - main
+
+concurrency:
+  # Skip intermediate builds: always.
+  # Cancel intermediate builds: only if it is a pull request build.
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: ${{ startsWith(github.ref, 'refs/pull/') }}
+
+permissions:
+  contents: write
+  pull-requests: read
+  statuses: write
+
+jobs:
+  docs:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+      - uses: julia-actions/setup-julia@latest
+        with:
+          version: '1'
+      - name: Install dependencies
+        run: julia --project=docs/ -e 'using Pkg; Pkg.develop(PackageSpec(path=pwd())); Pkg.instantiate()'
+      - name: Build and deploy
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} # For authentication with GitHub Actions token
+          DOCUMENTER_KEY: ${{ secrets.DOCUMENTER_KEY }} # For authentication with SSH deploy key
+          JULIA_DEBUG: Documenter # Print `@debug` statements (https://github.com/JuliaDocs/Documenter.jl/issues/955)
+        run: julia --project=docs/ docs/make.jl
diff --git a/.github/workflows/DocsNav.yml b/.github/workflows/DocsNav.yml
new file mode 100644
index 0000000..14614d1
--- /dev/null
+++ b/.github/workflows/DocsNav.yml
@@ -0,0 +1,49 @@
+name: Add Navbar
+
+on:
+  page_build:  # Triggers the workflow on push events to gh-pages branch
+  workflow_dispatch:  # Allows manual triggering
+  schedule:
+    - cron: '0 0 * * 0'  # Runs every week on Sunday at midnight (UTC)
+
+jobs:
+  add-navbar:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+    steps:
+      - name: Checkout gh-pages
+        uses: actions/checkout@v4
+        with:
+          ref: gh-pages
+          fetch-depth: 0
+
+      - name: Download insert_navbar.sh
+        run: |
+          curl -O https://raw.githubusercontent.com/TuringLang/turinglang.github.io/main/assets/scripts/insert_navbar.sh
+          chmod +x insert_navbar.sh
+
+      - name: Update Navbar
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          git config user.name github-actions[bot]
+          git config user.email github-actions[bot]@users.noreply.github.com
+
+          # Define the URL of the navbar to be used
+          NAVBAR_URL="https://raw.githubusercontent.com/TuringLang/turinglang.github.io/main/assets/scripts/TuringNavbar.html"
+         
+          # Update all HTML files in the current directory (gh-pages root)
+          ./insert_navbar.sh . $NAVBAR_URL
+         
+          # Remove the insert_navbar.sh file
+          rm insert_navbar.sh
+         
+          # Check if there are any changes
+          if [[ -n $(git status -s) ]]; then
+            git add .
+            git commit -m "Added navbar and removed insert_navbar.sh"
+            git push "https://${GITHUB_ACTOR}:${GITHUB_TOKEN}@github.com/${GITHUB_REPOSITORY}.git" gh-pages
+          else
+            echo "No changes to commit"
+          fi
diff --git a/.github/workflows/TagBot.yml b/.github/workflows/TagBot.yml
index 778c06f..f49313b 100644
--- a/.github/workflows/TagBot.yml
+++ b/.github/workflows/TagBot.yml
@@ -12,3 +12,4 @@ jobs:
       - uses: JuliaRegistries/TagBot@v1
         with:
           token: ${{ secrets.GITHUB_TOKEN }}
+          ssh: ${{ secrets.DOCUMENTER_KEY }}
diff --git a/.gitignore b/.gitignore
index d93db51..4389dcf 100644
--- a/.gitignore
+++ b/.gitignore
@@ -24,4 +24,6 @@ docs/site/
 Manifest.toml
 
 # vs code environment
-.vscode
\ No newline at end of file
+.vscode
+
+.DS_Store
diff --git a/docs/Project.toml b/docs/Project.toml
new file mode 100644
index 0000000..dfa65cd
--- /dev/null
+++ b/docs/Project.toml
@@ -0,0 +1,2 @@
+[deps]
+Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4"
diff --git a/docs/make.jl b/docs/make.jl
new file mode 100644
index 0000000..404169e
--- /dev/null
+++ b/docs/make.jl
@@ -0,0 +1,18 @@
+using Documenter
+using AbstractPPL
+
+# Doctest setup
+DocMeta.setdocmeta!(AbstractPPL, :DocTestSetup, :(using AbstractPPL); recursive=true)
+
+makedocs(;
+    sitename="AbstractPPL",
+    modules=[AbstractPPL],
+    pages=[
+        "Home" => "index.md",
+        "API" => "api.md",
+    ],
+    checkdocs=:exports,
+    doctest=false,
+)
+
+deploydocs(; repo="github.com/TuringLang/AbstractPPL.jl.git", push_preview=true)
diff --git a/docs/src/api.md b/docs/src/api.md
new file mode 100644
index 0000000..a8d4321
--- /dev/null
+++ b/docs/src/api.md
@@ -0,0 +1,32 @@
+# API
+
+## VarNames
+
+```@docs
+VarName
+getsym
+getoptic
+inspace
+subsumes
+subsumedby
+vsym
+@varname
+@vsym
+```
+
+## Abstract model functions
+
+```@docs
+AbstractProbabilisticProgram
+condition
+decondition
+logdensityof
+AbstractContext
+evaluate!!
+```
+
+## Abstract traces
+
+```@docs
+AbstractModelTrace
+```
diff --git a/docs/src/index.md b/docs/src/index.md
new file mode 100644
index 0000000..03c3112
--- /dev/null
+++ b/docs/src/index.md
@@ -0,0 +1,3 @@
+# AbstractPPL.jl
+
+A lightweight package containing interfaces and associated APIs for modelling languages for probabilistic programming.
diff --git a/src/varname.jl b/src/varname.jl
index 1ffa542..da1bf02 100644
--- a/src/varname.jl
+++ b/src/varname.jl
@@ -211,7 +211,7 @@ Base.Symbol(vn::VarName) = Symbol(string(vn))  # simplified symbol
     inspace(vn::Union{VarName, Symbol}, space::Tuple)
 
 Check whether `vn`'s variable symbol is in `space`.  The empty tuple counts as the "universal space"
-containing all variables. Subsumption (see [`subsume`](@ref)) is respected.
+containing all variables. Subsumption (see [`subsumes`](@ref)) is respected.
 
 ## Examples
 
@@ -322,6 +322,11 @@ subsumes(
 ) = subsumes_indices(t, u)
 
 
+"""
+    subsumedby(t, u)
+
+True if `t` is subsumed by `u`, i.e., if `subsumes(u, t)` is true.
+"""
 subsumedby(t, u) = subsumes(u, t)
 uncomparable(t, u) = t ⋢ u && u ⋢ t
 const ⊒ = subsumes
@@ -513,7 +518,7 @@ julia> y = zeros(10, 10);
 julia> @varname(y[:], true)
 y[:]
 
-julia> # The underlying value is conretized, though:
+julia> # The underlying value is concretized, though:
        AbstractPPL.getoptic(AbstractPPL.concretize(@varname(y[:]), y)).indices[1]
 ConcretizedSlice(Base.OneTo(100))
 ```
@@ -525,11 +530,11 @@ concretize(vn::VarName, x) = VarName(vn, concretize(getoptic(vn), x))
 
 A macro that returns an instance of [`VarName`](@ref) given a symbol or indexing expression `expr`.
 
-If `concretize` is `true`, the resulting expression will be wrapped in a [`concretize`](@ref) call.
+If `concretize` is `true`, the resulting expression will be wrapped in a `concretize()` call.
 
 Note that expressions involving dynamic indexing, i.e. `begin` and/or `end`, will always need to be
 concretized as `VarName` only supports non-dynamic indexing as determined by
-[`is_static_index`](@ref). See examples below.
+`is_static_optic`. See examples below.
 
 ## Examples