\documentclass[a4paper,11pt]{article}

\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{array}
\usepackage[scaled=.85]{beramono}
\usepackage{booktabs}
%\usepackage{cite}
\usepackage[table,dvipsnames]{xcolor}
\usepackage{datetime}
\usepackage{eurosym}
\usepackage[sfdefault]{FiraSans}
\usepackage{mathtools}
\usepackage{multirow}
\usepackage[sort]{natbib}
\usepackage{pdfpages}
\usepackage[nottoc,numbib]{tocbibind}
\usepackage{url}
\usepackage{version}
\usepackage{graphicx}
\usepackage[normalem]{ulem}
\usepackage{rotating}

\usepackage[
   a4paper,
   pdftex,
%   pdftitle={Course Redesign},
   pdfauthor={Jasmin Blanchette},
   pdfkeywords={},
   pdfborder={0 0 0},
   draft=false,
   bookmarksnumbered,
   bookmarks,
   bookmarksdepth=2,
   bookmarksopenlevel=2,
   bookmarksopen]{hyperref}

\oddsidemargin=7.6mm
\evensidemargin=7.6mm
\textwidth=144mm
\topmargin=5.6mm
\headheight=0mm
\headsep=0mm
\textheight=232mm

\newcommand\legend{%
\vfill
%Legend:
%
\noindent
{\small\begin{tabular}{@{}r@{}l@{}}
AB & ~~=~~Anne Baanen~\,(teaching assistant) \\
HG & ~~=~~\emph{The Hitchhiker's Guide to Logical Verification} \\
JB & ~~=~~Jasmin Blanchette~\,(lecturer) \\
JL & ~~=~~Jannis Limperg~\,(teaching assistant) \\
LoVe & ~~=~~Logical Verification \\
RL & ~~=~~Robert Y. Lewis~\,(guest lecturer) \\
VN & ~~=~~Visa Nummelin~\,(lecturer) \\
\end{tabular}}
\pagebreak}

\begin{document}
  
\pagestyle{empty}

\noindent
{\Large\bfseries Logical Verification 2021--2022 \\[\jot]
Course Overview}

\bigskip

\newcolumntype{E}{>{\raggedright\arraybackslash}p{0.75cm}}
\newcolumntype{F}{>{\raggedright\arraybackslash}p{1.25cm}}
\newcolumntype{G}{>{\raggedright\arraybackslash}p{1.55cm}}
\newcolumntype{H}{>{\raggedright\arraybackslash}p{4.725cm}}
\newcolumntype{I}{>{\raggedright\arraybackslash}p{4.475cm}}

\definecolor{verylightgray}{rgb}{0.85,0.85,0.85}
\renewcommand\lg{\cellcolor{verylightgray}}

\newcommand\bef{\vphantom{$(^{(^{(}}$}}
\newcommand\aft{\vphantom{$(_{(_{(}}$}}

\bigskip

\subsection*{\strut Part I: Basics}

\begingroup
\footnotesize
\noindent
\begin{tabular}{EFGHI}
\toprule
\bf Block & \bf Session & \bf Educators & \bf In-class & \bf Out-class \\
\midrule
1 & \bef Lecture~1 & JB
  & $\bullet$~introduce~LoVe\phantom{xxx}
    $\bullet$~introduce~Lean
    $\bullet$~review~Lean~as~a~functional
    \phantom{$\bullet$~}programming~language\aft
  & $\bullet$~read~preface~and~Ch.~1~of~HG
    $\bullet$~review~demo~1
    \llap{[}$\bullet$~read~Haskell~tutorial~if
    \phantom{$\bullet$~}needed\,]
\\
\bef
  & \lg \bef Lab~1 & \lg JB, AB, JL
  & \lg $\bullet$~explain basics of VS Code
        $\bullet$~explain basic Lean syntax
        $\bullet$~help~with~exercise~1
  & \lg $\bullet$~install~VS~Code,~Lean,
        \phantom{$\bullet$~}\verb|mathlib|\phantom{xxxxxxxxxxxxxx}
        $\bullet$~clone LoVe repository
        $\bullet$~do~exercise~1
        $\bullet$~do~homework~1 (by~lecture~3)\aft \\
\midrule
2 & \bef Lecture~2 & JB
  & $\bullet$~explain~backward~proofs
    \phantom{$\bullet$~}in~math,~Lean
    $\bullet$~introduce~basic~tactics
    $\bullet$~\hbox{demo}~mathematical~induction\aft
  & $\bullet$~read~Ch.~2~of~HG
    $\bullet$~review~demo~2 \\
\bef
  & \lg \bef Lab~2 & \lg JB, AB, JL
  & \lg $\bullet$~help~with~exercise~2
  & \lg $\bullet$~do~exercise~2
        $\bullet$~do~homework~2~(by~lecture~4)\aft \\
\midrule
3 & \bef Lecture~3 & JB
  & $\bullet$~explain~forward~proofs
    \phantom{$\bullet$~}in~math,~Lean
    $\bullet$~introduce~calculational~proofs
    $\bullet$~explain~dependent~types
    $\bullet$~unveil~Curry--Howard
    $\bullet$~explain~induction~by
    \phantom{$\bullet$~}pattern~matching\aft
  & $\bullet$~read~Ch.~3~of~HG
    $\bullet$~review~demo~3 \\
\bef
  & \lg \bef Lab~3 & \lg AB, JL, VN
  & \lg $\bullet$~help~with~exercise~3
  & \lg $\bullet$~do~exercise~3
        $\bullet$~do~homework~3~(by~lecture~5)\aft \\
\bottomrule
\end{tabular}
\endgroup

\legend

\subsection*{\strut Part II: Functional--Logic Programming}

\begingroup
\footnotesize
\noindent
\begin{tabular}{EFGHI}
\toprule
\bf Block & \bf Session & \bf Educators & \bf In-class & \bf Out-class \\
\midrule
4 & \bef Lecture~4 & JB
  & $\bullet$~take~a~closer~look~at
    \phantom{$\bullet$~}recursion~and~induction
    $\bullet$~\hbox{introduce~structures},
    \phantom{$\bullet$~}type~classes
  \aft
  & $\bullet$~read~Ch.~4~of~HG
    $\bullet$~review~demo~4 \\
\bef
  & \lg \bef Lab~4 & \lg AB, VL
  & \lg $\bullet$~help~with~exercise~4
  & \lg $\bullet$~do~exercise~4
        $\bullet$~do~homework~4~(by~lecture~6)\aft \\
\midrule
5 & \bef Lecture~5 & JB
  & $\bullet$~explain~meaning~of
    \phantom{$\bullet$~}inductive~predicates
    $\bullet$~present~many~examples
    $\bullet$~\hbox{explain}~induction,~elimination
  \aft
  & $\bullet$~read~Ch.~5~of~HG
    $\bullet$~review~demo~5 \\
\bef
  & \lg \bef Lab~5 & \lg JB, JL
  & \lg $\bullet$~help~with~exercise~5
  & \lg $\bullet$~do~exercise~5
        $\bullet$~do~homework~5~(by~lecture~7)\aft \\
\midrule
6 & \bef Lecture~6 & JB
  & $\bullet$~introduce~monads\phantom{xxxxxxxxxx}
    $\bullet$~present~\verb|id|, \verb|option|, \verb|action|, \verb|set|
    $\bullet$~review~a~monadic~algorithm
  \aft
  & $\bullet$~read~Ch.~6~of~HG
    $\bullet$~review~demo~6 \\
\bef
  & \lg \bef Lab~6 & \lg AB, JB
  & \lg $\bullet$~help~with~exercise~6
  & \lg $\bullet$~do~exercise~6
        $\bullet$~do~homework~6~(by~lecture~8)\aft \\
\midrule
7 & \bef Lecture~7 & JB
  & $\bullet$~introduce~tactic~combinators
    $\bullet$~introduce~\verb|tactic|~monad
    $\bullet$~present~expression~API
    $\bullet$~walk~through~examples\aft
  & $\bullet$~read~Ch.~7~of~HG
    $\bullet$~review~demo~7 \\
\bef
  & \lg \bef Lab~7 & \lg JL, VN
  & \lg $\bullet$~help~with~exercise~7
  & \lg $\bullet$~do~exercise~7
        $\bullet$~do~homework~7~(by~lecture~9)\aft \\
\bottomrule
\end{tabular}
\endgroup

\legend

\subsection*{\strut Part III: Program Semantics}

\begingroup
\footnotesize
\noindent
\begin{tabular}{EFGHI}
\toprule
\bf Block & \bf Session & \bf Educators & \bf In-class & \bf Out-class \\
\midrule
8 & \bef Lecture~8 & JB
  & $\bullet$~motivate~formal~semantics
    $\bullet$~present~WHILE~language
    $\bullet$~show~big-step~semantics~in
    \phantom{$\bullet$~}math,~Lean
    $\bullet$~show~small-step~semantics~in
    \phantom{$\bullet$~}math,~Lean\phantom{xxxxxxx}
    $\bullet$~discuss~parallelism\aft
  & $\bullet$~read~Ch.~8~of~HG
    $\bullet$~review~demo~8 \\
\bef
  & \lg \bef Lab~8 & \lg AB, JL
  & \lg $\bullet$~help~with~exercise~8
  & \lg $\bullet$~install~VS~Code~and~Lean
        $\bullet$~clone the LoVe repository
        $\bullet$~do~exercise~8\phantom{xxxxxx}
        $\bullet$~do~homework~8~(by~lecture~10)\aft \\
\midrule
9 & \bef Lecture~9 & JB
  & $\bullet$~introduce~Hoare~triples
    $\bullet$~present~Hoare~rules
    $\bullet$~show~Lean~definition
    $\bullet$~show~examples
    $\bullet$~introduce~and~demo~VCG\aft
  & $\bullet$~read~Ch.~9~of~HG
    $\bullet$~review~demo~9 \\
\bef
  & \lg \bef Lab~9 & \lg JB, JL
  & \lg $\bullet$~help~with~exercise~9
        $\bullet$~help~with~project
  & \lg $\bullet$~do~exercise~9
        $\bullet$~do~homework~9~(by~lecture~11)
        \phantom{$\bullet$~}or~project~(by~lecture~12)\aft \\
\midrule
10 & \bef Lecture~10 & JB
  & $\bullet$~introduce~denotational~semantics
    $\bullet$~explain~fixpoints
    $\bullet$~discuss~applications~to
    \phantom{$\bullet$~}program~equivalence\aft
  & $\bullet$~read~Ch.~10~of~HG
    $\bullet$~review~demo~10 \\
\bef
  & \lg \bef Lab~10 & \lg JB, AB
  & \lg $\bullet$~help~with~exercise~10
        $\bullet$~help~with~project
  & \lg $\bullet$~do~exercise~10
        $\bullet$~do~homework~10~or~project
        \phantom{$\bullet$~}(by~lecture~12)\aft \\
\bottomrule
\end{tabular}
\endgroup

\legend

\subsection*{\strut Part IV: Mathematics}

\begingroup
\footnotesize
\noindent
\begin{tabular}{EFGHI}
\toprule
\bf Block & \bf Session & \bf Educators & \bf In-class & \bf Out-class \\
\midrule
11 & \bef Lecture~11 & JB
  & $\bullet$~present~universes
    $\bullet$~explain~\verb|Prop|'s~peculiarities
    $\bullet$~review~the~axiom~of~choice
    $\bullet$~explain~subtypes,~quotients\aft
  & $\bullet$~read~Ch.~11~of~HG
    $\bullet$~review~demo~11 \\
\bef
  & \lg \bef Lab~11 & \lg JL, VN
  & \lg $\bullet$~help~with~exercise~11
  & \lg $\bullet$~do~exercise~11
        \llap{[}$\bullet$~do~homework~11
        \phantom{$\bullet$~}(by~lecture~13)\,]\aft \\
\midrule
12 & \bef Lecture~12 & JB
  & $\bullet$~present~groups,~fields,~rings
    $\bullet$~present~coercions,
    \phantom{$\bullet$~}normalizations
    $\bullet$~\hbox{contrast}~lists,~multisets,~finsets
    $\bullet$~present~orders\aft
  & $\bullet$~read~Ch.~12~of~HG
    $\bullet$~review~demo~12 \\
\bef
  & \lg \bef Lab~12 & \lg JB, VN
  & \lg $\bullet$~help~with~exercise~12
  & \lg $\bullet$~do~exercise~12
        $\bullet$~start~revising~for~final~exam\aft \\
\midrule
13 & \bef Lecture~13 & VN
  & $\bullet$~review~construction~of~$\mathbb{Q}$
    $\bullet$~review~construction~of~$\mathbb{R}$
    $\bullet$~\hbox{discuss}~alternatives
    $\bullet$~have~students~present~projects\aft
  & $\bullet$~read~Ch.~13~of~HG
    $\bullet$~review~demo~13
    $\bullet$~revise~for~final~exam \\
\bef
  & \lg \bef Lab~13 & \lg AB, VN
  & \lg $\bullet$~help~with~exercise~13
        $\bullet$~answer~exam-related~questions
  & \lg $\bullet$~do~exercise~13
        $\bullet$~revise~for~final~exam\aft \\
\midrule
14 & \bef Guest lecture & RL
  & $\bullet$~introduce~\textit{p}-adics
    $\bullet$~present~\textit{p}-adics~in~Lean\aft
  & $\bullet$~skim~RL's~paper~on~\textit{p}-adics
    $\bullet$~revise~for~final~exam\aft \\
\bef
  & \lg \bef Lab~14 & \lg JB
  & \lg $\bullet$~answer~exam-related~questions
  & \lg $\bullet$~revise~for~final~exam\aft \\
\bottomrule
\end{tabular}
\endgroup

\legend

\end{document}
