Summary

Preamble

import Chapter.Preamble.Demo
import Chapter.Preamble.Setup

Functions and data

import Chapter.Intro.Lambda
import Chapter.Intro.Bool
import Chapter.Intro.Bool.Properties
import Chapter.Intro.NaturalNumbers
import Chapter.Intro.Polymorphism
import Chapter.Intro.Lists

Constructive logic

import Chapter.Logic.Connectives
import Chapter.Logic.Negation
import Chapter.Logic.Existential
import Chapter.Logic.Predicates
import Chapter.Logic.Equality
import Chapter.Logic.LessThan

Verification of functional programs

import Chapter.Fun.SortedLists
import Chapter.Fun.ExtrinsicInsertionSort
import Chapter.Fun.IntrinsicInsertionSort

Verification of imperative programs

import Chapter.Imp.Introduction
import Chapter.Imp.AexpBexp
import Chapter.Imp.BigStep
import Chapter.Imp.SmallStep
import Chapter.Imp.HoareLogic
import Chapter.Imp.HoareLogicExample
import Chapter.Imp.HoareLogicSoundness
import Chapter.Imp.HoareLogicCompleteness
import Chapter.Imp.VerificationConditions

Appendix: mini Agda library

import Library.Bool
import Library.Equality
import Library.Equality.Reasoning
import Library.Fun
import Library.LessThan
import Library.LessThan.Alternative
import Library.LessThan.Reasoning
import Library.List
import Library.List.Permutation
import Library.List.Properties
import Library.List.Sorted
import Library.Logic
import Library.Logic.Laws
import Library.Nat
import Library.Nat.Properties
import Library.WellFounded