\documentclass{article}

\input{~/projects/latex/janishutz-helpers.tex}

\usepackage{tikz}
\usetikzlibrary{positioning, arrows.meta}

\usepackage{lmodern}
\usepackage{ebproof}
\usepackage{overarrows}
\usepackage{bm}

\NewOverArrowCommand{\overrightharpoon}{%
    end=\rightharpoonup
}
\ebproofset{separation=2.5em}
\setFontType{sans}
\multicolsep 5pt plus 2pt minus 2pt

\setcounter{secnumdepth}{5}
\makeatletter
\renewcommand\subparagraph{%
    \@startsection{subparagraph}{5}{0mm}%
    {-.5\baselineskip}%
    {.25\baselineskip}%
    {\normalfont\normalsize\bfseries}}
\makeatother

\setup{Formal Methods \& Functional Programming}

% ────────────────────────────────────────────────────────────────────

\begin{document}
\startDocument
\mediumverticalspacing

\vspace{1cm}
\[
    \begin{prooftree}
        \infer0{\Gamma \vdash z :: \sigma \rightarrow (\tau_2, \tau_3)}
        \infer0{\Gamma \vdash y :: \sigma}
        \infer2[App]{\Gamma \vdash (z\; y) :: (\tau_2, \tau_3)}
        \infer1[fst]{\Gamma = y : \texttt{Int}, z : \tau_1 \vdash \texttt{fst}\; (z\; y) :: \tau_2}
        \infer1[Abs]{y : \texttt{Int} \vdash \lambda z. \texttt{fst}\; (z\; y) :: \tau_0}
        \infer1[Abs]{\vdash \lambda y.\lambda z. \texttt{fst}\; (z\; y) :: \texttt{Int} \rightarrow \tau_0}
        %
        \infer0[Int]{\vdash 0 :: \texttt{Int}}
        \infer2[App]{\vdash (\lambda y.\lambda z. \texttt{fst}\; (z\; y))\; 0 :: \tau_0}
    \end{prooftree}
\]
\vspace{0.1cm}
\begin{center}
    \begin{minipage}{0.2\linewidth}
        Constraints:
        \begin{itemize}
            \item $\tau_0 = \tau_1 \rightarrow \tau_2$
            \item $\tau_1 = \sigma \rightarrow (\tau_2, \tau_3)$
            \item $\tau_2 = \sigma = \texttt{Int}$
        \end{itemize}
    \end{minipage}

    Thus: $\tau_0 = \texttt{Int} \rightarrow (\tau_2, \tau_3) \rightarrow \tau_2$
\end{center}


\vspace{3cm}
\begin{center}
    \begin{Large}
        \quote{A funny quote by a professor - If you know one, please let me know}
    \end{Large}

    \hspace{3cm} - Prof. Dr. Professor Name, 2026
\end{center}

\vspace{1.5cm}
\begin{center}
    FS2026, ETHZ

    \begin{Large}
        Summary of the Lecture Slides,\\
        Overview over common exercise types
    \end{Large}

    \url{https://infsec.ethz.ch/education/ss2026/fmfp.html}
\end{center}


\newpage
\printtoc{Aquamarine}

% TODO: Strong and weak structural induction and more


\newsection
\section{Haskell}
\input{parts/00_haskell/00_intro.tex}
\input{parts/00_haskell/01_syntax.tex}


\newsection
\section{Induction Proofs}
\label{sec:induction-proofs}
\input{parts/01_induction-proofs/00_intro.tex}
\input{parts/01_induction-proofs/01_mathematical-induction.tex}
\input{parts/01_induction-proofs/02_structural-induction.tex}
\input{parts/01_induction-proofs/03_induction-on-trees.tex}
\input{parts/01_induction-proofs/04_other-induction.tex}
\input{parts/01_induction-proofs/05_induction-on-proof-trees.tex}
\input{parts/01_induction-proofs/06_induction-on-derivation-sequence.tex}
\input{parts/01_induction-proofs/07_workflow.tex}
\input{parts/01_induction-proofs/08_cyp.tex}
% \input{parts/01_induction-proofs/}

\newsection
\section{Formal Reasoning}
\input{parts/02_formal-reasoning/00_formal-proofs.tex}
\input{parts/02_formal-reasoning/01_natural-deduction.tex}
\input{parts/02_formal-reasoning/02_propositional-logic/00_syntax.tex}
\input{parts/02_formal-reasoning/02_propositional-logic/01_semantics.tex}
\input{parts/02_formal-reasoning/02_propositional-logic/02_deductive-system.tex}
\input{parts/02_formal-reasoning/02_propositional-logic/03_natural-deduction-prop-logic.tex}
\input{parts/02_formal-reasoning/02_propositional-logic/04_derivation-rules-overview.tex}
\input{parts/02_formal-reasoning/03_first-order-logic/00_syntax.tex}
\input{parts/02_formal-reasoning/03_first-order-logic/01_semantics.tex}
\input{parts/02_formal-reasoning/03_first-order-logic/02_quantifiers.tex}
\input{parts/02_formal-reasoning/04_equality.tex}
\input{parts/02_formal-reasoning/05_correctness/00_intro.tex}
\input{parts/02_formal-reasoning/05_correctness/01_termination.tex}
\input{parts/02_formal-reasoning/05_correctness/02_behaviour.tex}
% \input{parts/02_formal-reasoning/05_correctness/}
% \input{parts/02_formal-reasoning/}


\newsection
\section{Typing}
\input{parts/03_typing/00_intro.tex}
\input{parts/03_typing/01_mini-haskell/00_syntax.tex}
\input{parts/03_typing/01_mini-haskell/01_lambda-calculus.tex}
\input{parts/03_typing/01_mini-haskell/02_further-rules.tex}
\input{parts/03_typing/01_mini-haskell/03_type-inference.tex}
\input{parts/03_typing/02_algebraic-data-types/00_correctness.tex}
\input{parts/03_typing/02_algebraic-data-types/01_induction-nat-num.tex}
\input{parts/03_typing/02_algebraic-data-types/02_lists.tex}
\input{parts/03_typing/02_algebraic-data-types/03_trees.tex}
\input{parts/03_typing/03_interpreter/00_intro.tex}
\input{parts/03_typing/03_interpreter/01_read.tex}
\input{parts/03_typing/03_interpreter/02_eval.tex}
% \input{parts/03_typing/03_interpreter/}


\newsection
\section{Language Semantics}
\input{parts/04_language-semantics/00_imp/00_syntax.tex}
\input{parts/04_language-semantics/00_imp/01_semantics.tex}
\input{parts/04_language-semantics/00_imp/02_properties.tex}
\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/00_transition-systems.tex}
\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/01_semantics.tex}
\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/02_instantiations.tex}
\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/03_termination.tex}
\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/04_semantic-equivalence.tex}
\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex}
\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex}
\input{parts/04_language-semantics/01_operational-semantics/00_big-step-semantics/07_extensions-of-imp.tex}
\input{parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/00_structural-operational-semantics.tex}
\input{parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/01_rules.tex}
\input{parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/02_multi-step-derivation-seq.tex}
\input{parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/03_termintation.tex}
\input{parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/04_proofs.tex}
\input{parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/05_semantic-equivalence.tex}
\input{parts/04_language-semantics/01_operational-semantics/01_small-step-semantics/06_extensions.tex}
\input{parts/04_language-semantics/01_operational-semantics/02_equiv.tex}
\input{parts/04_language-semantics/01_operational-semantics/03_rules-summary.tex}
\input{parts/04_language-semantics/02_axiomatic-semantics/00_intro.tex}
\input{parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex}
\input{parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/01_derivation-systems.tex}
\input{parts/04_language-semantics/02_axiomatic-semantics/01_hoare-logic/02_total-correctness.tex}
\input{parts/04_language-semantics/02_axiomatic-semantics/02_soundness-completeness.tex}
% \input{parts/04_language-semantics/}

\newsection
\section{Modelling}
\input{parts/05_modelling/00_intro.tex}
\input{parts/05_modelling/01_promela/00_syntax.tex}
\input{parts/05_modelling/01_promela/01_expressions.tex}
\input{parts/05_modelling/01_promela/02_statements.tex}
\input{parts/05_modelling/01_promela/03_macros.tex}
\input{parts/05_modelling/02_linear-temporal-logic/00_linear-time-properties.tex}
\input{parts/05_modelling/02_linear-temporal-logic/01_linear-temporal-logic.tex}
% \input{parts/05_modelling/02_linear-temporal-logic/}
% \input{parts/05_modelling/}


\newsection
\section{Exercises}
\subsection{Introduction}
\input{parts/06_exercises/00_intro.tex}

\subsection{Functional Programming}
\input{parts/06_exercises/01_fp/00_eval-strats.tex}
\input{parts/06_exercises/01_fp/01_haskell.tex}
\input{parts/06_exercises/01_fp/02_natural-deduction.tex}
\input{parts/06_exercises/01_fp/03_type-inference.tex}
% \input{parts/06_exercises/01_fp/}

\subsection{Induction}
For induction proofs, see Section~\ref{sec:induction-proofs}, which were moved up, since they are used in both FP and FM,
as well as being mentioned a few times in the rest of the summary.

\newpage
\subsection{Formal Methods}
\input{parts/06_exercises/02_fm/00_imp.tex}
\input{parts/06_exercises/02_fm/01_operational-semantics.tex}
\input{parts/06_exercises/02_fm/02_axiomatic-semantics.tex}
\input{parts/06_exercises/02_fm/03_modelling.tex}
\input{parts/06_exercises/02_fm/04_ltl.tex}
% \input{parts/06_exercises/02_fm/}
% \input{parts/06_exercises/}

\newpage
\input{parts/06_exercises/03_checklist.tex}


\end{document}