Software-Foundations-Checklist

A checklist of the exercises I have completed in the Software Foundations series.

Why a checklist? Why not a collection of solutions?

Software Foundations - Volume 1: Logical Foundations - Preface - Practicalities - Exercises explicitly requests its readers not to share solutions online in order not to spoil any university courses that may utilize it as a teaching resource or course curriculum:

Please do not post solutions to the exercises in a public place.

Completed Volumes

• Volume 1: Logical Foundations
• Volume 2: Programming Language Foundations
• Volume 3: Verified Functional Algorithms
  • Note: the incomplete proofs delete_max_Some_priq, delete_max_None_relate, and delete_max_Some_relate are also unsolved by the volume's author, Andrew Appel
• Volume 6: Separation Logic Foundations

In-Progress Volumes

Check back later!

The Checklist

• Volume 1: Logical Foundations
• • Functional Programming in Coq
• • • Data and Functions
• • • • Booleans
• • • • • Exercise: 1 star, standard (nandb)
• • • • • Exercise: 1 star, standard (andb3)
• • • • Numbers
• • • • • Exercise: 1 star, standard (factorial)
• • • • • Exercise: 1 star, standard (ltb)
• • • Proof by Rewriting
• • • • Exercise: 1 star, standard (plus_id_exercise)
• • • • Exercise: 2 stars, standard (mult_S_1)
• • • Proof by Case Analysis
• • • • Exercise: 2 stars, standard (andb_true_elim2)
• • • • Exercise: 1 star, standard (zero_nbeq_plus_1)
• • • • Fixpoints and Structural Recursion (Optional)
• • • • • Exercise: 2 stars, standard, optional (decreasing)
• • • More Exercises
• • • • Exercise: 1 star, standard (indentity_fn_applied_twice)
• • • • Exercise: 1 star, standard (negation_fn_applied_twice)
• • • • Exercise: 3 stars, standard, optional (andb_eq_orb)
• • • • Exercise: 3 stars, standard (binary)
• • Proof by Induction
• • • Proof by Induction
• • • • Exercise: 2 stars, standard, recommended (basic_induction)
• • • • Exercise: 2 stars, standard (double_plus)
• • • • Exercise: 2 stars, standard, optional (evenb_S)
• • • • Exercise: 1 star, standard (destruct_induction)
• • • Formal vs. Informal Proof
• • • • Exercise: 2 stars, advanced, recommended (plus_comm_informal)
• • • • Exercise: 2 stars, standard, optional (eqb_refl_informal)
• • • More Exercises
• • • • Exercise: 3 stars, standard, recommended (mult_comm)
• • • • Exercise: 3 stars, standard, optional (more_exercises)
• • • • Exercise: 2 stars, standard, optional (eqb_refl)
• • • • Exercise: 2 stars, standard, optional (plus_swap')
• • • • Exercise: 3 stars, standard, recommended (binary_commute)
• • • • Exercise: 5 stars, advanced (binary_inverse)
• • Working with Structured Data
• • • Pairs of Numbers
• • • • Exercise: 1 star, standard (snd_fst_is_swap)
• • • • Exercise: 1 star, standard, optional (fst_swap_is_snd)
• • • Lists of Numbers
• • • • Exercises
• • • • • Exercise: 2 stars, standard, recommended (list_funs)
• • • • • Exercise: 3 stars, advanced (alternate)
• • • • Bags via Lists
• • • • • Exercise: 3 stars, standard, recommended (bag_functions)
• • • • • Exercise: 3 stars, standard, optional (bag_more_functions)
• • • • • Exercise: 2 stars, standard, recommended (bag_theorem)
• • • Reasoning About Lists
• • • • List Exercises, Part 1
• • • • • Exercise: 3 stars, standard (list_exercises)
• • • • • Exercise: 2 stars, standard (eqblist)
• • • • List Exercises, Part 2
• • • • • Exercise: 1 star, standard (count_member_nonzero)
• • • • • Exercise: 3 stars, advanced (remove_does_not_increase_count)
• • • • • Exercise: 3 stars, standard, optional (bag_count_sum)
• • • • • Exercise: 4 stars, advanced (rev_injective)
• • • Options
• • • • Exercise: 2 stars, standard (hd_error)
• • • • Exercise: 1 star, standard, optional (option_elim_hd)
• • • Partial Maps
• • • • Exercise: 1 star, standard (eqb_id_refl)
• • • • Exercise: 1 star, standard (update_eq)
• • • • Exercise: 1 star, standard (update_neq)
• • • • Exercise: 2 stars, standard (baz_num_elts)
• • Polymorphism and Higher-Order Functions
• • • Polymorphism
• • • • Polymorphic Lists
• • • • • Exercise: 2 stars, standard (mumble_grumble)
• • • • • Exercises
• • • • • • Exercise: 2 stars, standard, optional (poly_exercises)
• • • • • • Exercise: 2 stars, standard, optional (more_poly_exercises)
• • • • Polymorphic Pairs
• • • • • Exercise: 1 star, standard, optional (combine_checks)
• • • • • Exercise: 2 stars, standard, recommended (split)
• • • • Polymorphic Options
• • • • • Exercise: 1 star, standard, optional (hd_error_poly)
• • • Functions as Data
• • • • Anonymous Functions
• • • • • Exercise: 2 stars, standard (filter_even_gt7)
• • • • • Exercise: 3 stars, standard (partition)
• • • • Map
• • • • • Exercises
• • • • • • Exercise: 3 stars, standard (map_rev)
• • • • • • Exercise: 2 stars, standard, recommended (flat_map)
• • • • • • Exercise: 2 stars, standard, optional (implicit_args)
• • • • Fold
• • • • • Exercise: 1 star, advanced (fold_types_different)
• • • Additional Exercises
• • • • Exercise: 2 stars, standard (fold_length)
• • • • Exercise: 3 stars, standard (fold_map)
• • • • Exercise: 2 stars, advanced (currying)
• • • • Exercise: 2 stars, advanced (nth_error_informal)
• • • • Exercise: 1 star, advanced (church_succ)
• • • • Exercise: 1 star, advanced (church_plus)
• • • • Exercise: 2 stars, advanced (church_mult)
• • • • Exercise: 2 stars, advanced (church_exp)
• • More Basic Tactics
• • • The apply tactic
• • • • Exercise: 2 stars, standard, optional (silly_ex)
• • • • Exercise: 3 stars, standard (apply_exercise1)
• • • • Exercise: 1 star, standard, optional (apply_rewrite)
• • • The apply with tactic
• • • • Exercise: 3 stars, standard, optional (apply_with_exercise)
• • • The injection and discriminate Tactics
• • • • Exercise: 1 star, standard (injection_ex3)
• • • • Exercise: 1 star, standard (discriminate_ex3)
• • • Using Tactics on Hypotheses
• • • • Exercise: 3 stars, standard, recommended (plus_n_n_injective)
• • • Varying the Induction Hypothesis
• • • • Exercise: 2 stars, standard (eqb_true)
• • • • Exercise: 2 stars, advanced (eqb_true_informal)
• • • • Exercise: 3 stars, standard, recommended (gen_dep_practice)
• • • Using destruct on Compound Expressions
• • • • Exercise: 3 stars, standard, optional (combine_split)
• • • • Exercise: 2 stars, standard (destruct_eqn_practice)
• • • Additional Exercises
• • • • Exercise: 3 stars, standard (eqb_sym)
• • • • Exercise: 3 stars, advanced, optional (eqb_sym_informal)
• • • • Exercise: 3 stars, standard, optional (eqb_trans)
• • • • Exercise: 3 stars, advanced (split_combine)
• • • • Exercise: 3 stars, advanced (filter_exercise)
• • • • Exercise: 4 stars, advanced, recommended (forall_exists_challenge)
• • Logic in Coq
• • • Logical Connectives
• • • • Conjunction
• • • • • Exercise: 2 stars, standard (and_exercise)
• • • • • Exercise: 1 star, standard, optional (proj2)
• • • • • Exercise: 2 stars, standard (and_assoc)
• • • • Disjunction
• • • • • Exercise: 1 star, standard (mult_eq_0)
• • • • • Exercise: 1 star, standard (or_commut)
• • • • Falsehood and Negation
• • • • • Exercise: 2 stars, standard, optional (not_implies_our_not)
• • • • • Exercise: 2 stars, advanced (double_neg_inf)
• • • • • Exercise: 2 stars, standard, recommended (contrapositive)
• • • • • Exercise: 1 star, standard (not_both_true_and_false)
• • • • • Exercise: 1 star, advanced (informal_not_PNP)
• • • • Logical Equivalence
• • • • • Exercise: 1 star, standard, optional (iff_properties)
• • • • • Exercise: 3 stars, standard (or_distributes_over_and)
• • • • Existential Quantification
• • • • • Exercise: 1 star, standard, recommended (dist_not_exists)
• • • • • Exercise: 2 stars, standard (dist_exists_or)
• • • Programming with Propositions
• • • • Exercise: 2 stars, standard (In_map_iff)
• • • • Exercise: 2 stars, standard (In_app_iff)
• • • • Exercise: 3 stars, standard, recommended (All)
• • • • Exercise: 3 stars, standard (combine_odd_even)
• • • Coq vs. Set Theory
• • • • Functional Extensionality
• • • • • Exercise: 4 stars, standard (tr_rev_correct)
• • • • Propositions and Booleans
• • • • • Exercise: 3 stars, standard (evenb_double_conv)
• • • • • Exercise: 2 stars, standard (logical_connectives)
• • • • • Exercise: 1 star, standard (eqb_neq)
• • • • • Exercise: 3 stars, standard (eqb_list)
• • • • • Exercise: 2 stars, standard, recommended (All_forallb)
• • • • Classical vs. Constructive Logic
• • • • • Exercise: 3 stars, standard (excluded_middle_irrefutable)
• • • • • Exercise: 3 stars, advanced (not_exists_dist)
• • • • • Exercise: 5 stars, standard, optional (classical_axioms)
• • Inductively Defined Propositions
• • • Inductively Defined Propositions
• • • • Inductive Definition of Evenness
• • • • • Exercise: 1 star, standard (ev_double)
• • • Using Evidence in Proofs
• • • • Inversion on Evidence
• • • • • Exercise: 1 star, standard (inversion_practice)
• • • • • Exercise: 1 star, standard (even5_nonsense)
• • • • Induction on Evidence
• • • • • Exercise: 2 stars, standard (ev_sum)
• • • • • Exercise: 4 stars, advanced, optional (even'_ev)
• • • • • Exercise: 3 stars, advanced, recommended (ev_ev__ev)
• • • • • Exercise: 3 stars, standard, optional (ev_plus_plus)
• • • Inductive Relations
• • • • Exercise: 2 stars, standard, optional (total_relation)
• • • • Exercise: 2 stars, standard, optional (empty_relation)
• • • • Exercise: 3 stars, standard, optional (le_exercises)
• • • • Exercise: 2 stars, standard, optional (leb_iff)
• • • • Exercise: 3 stars, standard, recommended (R_provability)
• • • • Exercise: 3 stars, standard, optional (R_fact)
• • • • Exercise: 2 stars, advanced (subsequence)
• • • • Exercise: 2 stars, standard, optional (R_provability2)
• • • Case Study: Regular Expressions
• • • • Exercise: 3 stars, standard (exp_match_ex1)
• • • • Exercise: 4 stars, standard, optional (reg_exp_of_list_spec)
• • • • Exercise: 4 stars, standard (re_not_empty)
• • • • The remember Tactic
• • • • • Exercise: 4 stars, standard, optional (exp_match_ex2)
• • • • • Exercise: 5 stars, advanced (pumping)
• • • Case Study: Improving Reflection
• • • • Exercise: 2 stars, standard, recommended (reflect_iff)
• • • • Exercise: 3 stars, standard, recommended (eqbP_practice)
• • • Additional Exercises
• • • • Exercise: 3 stars, standard, recommended (nostutter_defn)
• • • • Exercise: 4 stars, advanced (filter_challenge)
• • • • Exercise: 5 stars, advanced, optional (filter_challenge_2)
• • • • Exercise: 4 stars, standard, optional (palindromes)
• • • • Exercise: 5 stars, standard, optional (palindrome_converse)
• • • • Exercise: 4 stars, advanced, optional (NoDup)
• • • • Exercise: 4 stars, advanced, optional (pigeonhole_principle)
• • • • Extended Exercise: A Verified Regular-Expression Matcher
• • • • • Exercise: 3 stars, standard, optional (app_ne)
• • • • • Exercise: 3 stars, standard, optional (star_ne)
• • • • • Exercise: 2 stars, standard, optional (match_eps)
• • • • • Exercise: 3 stars, standard, optional (match_eps_refl)
• • • • • Exercise: 3 stars, standard, optional (derive)
• • • • • Exercise: 4 stars, standard, optional (derive_corr)
• • • • • Exercise: 2 stars, standard, optional (regex_match)
• • • • • Exercise: 3 stars, standard, optional (regex_refl)
• • Total and Partial Maps
• • • Total Maps
• • • • Exercise: 1 star, standard, optional (t_apply_empty)
• • • • Exercise: 2 stars, standard, optional (t_update_eq)
• • • • Exercise: 2 stars, standard, optional (t_update_neq)
• • • • Exercise: 2 stars, standard, optional (t_update_shadow)
• • • • Exercise: 2 stars, standard, optional (eqb_stringP)
• • • • Exercise: 2 stars, standard (t_update_same)
• • • • Exercise: 3 stars, standard, recommended (t_update_permute)
• • The Curry-Howard Correspondence
• • • Proof Scripts
• • • • Exercise: 2 stars, standard (eight_is_even)
• • • Logical Connectives as Inductive Types
• • • • Conjunction
• • • • • Exercise: 2 stars, standard, optional (conj_fact)
• • • • Disjunction
• • • • • Exercise: 2 stars, standard, optional (or_commut'')
• • • • Existential Quantification
• • • • • Exercise: 2 stars, standard, optional (ex_ev_Sn)
• • • Equality
• • • • Exercise: 2 stars, standard (equality__leibniz_equality)
• • • • Exercise: 5 stars, standard, optional (leibniz_equality__equality)
• • Induction Principles
• • • Basics
• • • • Exercise: 2 stars, standard, optional (plus_one_r')
• • • • Exercise: 1 star, standard, optional (rgb)
• • • • Exercise: 1 star, standard, optional (natlist1)
• • • • Exercise: 1 star, standard, optional (byntree_ind)
• • • • Exercise: 1 star, standard, optional (ex_set)
• • • Polymorphism
• • • • Exercise: 1 star, standard, optional (tree)
• • • • Exercise: 1 star, standard, optional (mytype)
• • • • Exercise: 1 star, standard, optional (foo)
• • • • Exercise: 1 star, standard, optional (foo')
• • • More on the induction Tactic
• • • • Exercise: 1 star, standard, optional (plus_explicit_prop)
• • Properties of Relations
• • • Basic Properties
• • • • Partial Functions
• • • • • Exercise: 2 stars, standard, optional (total_relation_not_partial)
• • • • • Exercise: 2 stars, standard, optional (empty_relation_partial)
• • • • Transitive Relations
• • • • • Exercise: 2 stars, standard, optional (le_trans_hard_way)
• • • • • Exercise: 2 stars, standard, optional (lt_trans'')
• • • • • Exercise: 1 star, standard, optional (le_S_n)
• • • • • Exercise: 2 stars, standard, optional (le_Sn_n_inf)
• • • • • Exercise: 1 star, standard, optional (le_Sn_n)
• • • • Symmetric and Antisymmetric Relations
• • • • • Exercise: 2 stars, standard, optional (le_not_symmetric)
• • • • • Exercise: 2 stars, standard, optional (le_antisymmetric)
• • • • • Exercise: 2 stars, standard, optional (le_step)
• • • Reflexive, Transitive Closure
• • • • Exercise: 2 stars, standard, optional (rsc_trans)
• • • • Exercise: 3 stars, standard, optional (rtc_rsc_coincide)
• • Simple Imperative Programs
• • • Coq Automation
• • • • Tacticals
• • • • • The repeat Tactical
• • • • • • Exercise: 3 stars, standard (optimize_0plus_b_sound)
• • • • • • Exercise: 4 stars, standard, optional (optimize)
• • • Evaluation as a Relation
• • • • Inference Rule Notation
• • • • • Exercise: 1 star, standard, optional (beval_rules)
• • • • Equivalence of the Definitions
• • • • • Exercise: 3 stars, standard (bevalR)
• • • Evaluating Commands
• • • • Evaluations as a Relation
• • • • • Operational Semantics
• • • • • • Exercise: 2 stars, standard (ceval_example2)
• • • • • • Exercise: 3 stars, standard, optional (pup_to_n)
• • • Reasoning About Imp Programs
• • • • Exercise: 3 stars, standard, recommended (XtimesYinZ_spec)
• • • • Exercise: 3 stars, standard, recommended (loop_never_stops)
• • • • Exercise: 3 stars, standard (no_whiles_eqv)
• • • • Exercise: 4 stars, standard (no_whiles_terminating)
• • • Additional Exercises
• • • • Exercise: 3 stars, standard (stack_compiler)
• • • • Exercise: 4 stars, advanced (stack_compiler_correct)
• • • • Exercise: 3 stars, standard, optional (short_circuit)
• • • • Exercise: 4 stars, advanced (break_imp)
• • • • Exercise: 3 stars, advanced, optional (while_break_true)
• • • • Exercise: 4 stars, advanced, optional (ceval_deterministic)
• • • • Exercise: 4 stars, standard, optional (add_for_loop)
• • An Evaluation Function for Imp
• • • A Step-Indexed Evaluator
• • • • Exercise: 2 stars, standard, recommended (pup_to_n)
• • • • Exercise: 2 stars, standard, optional (peven)
• • • Relational vs. Step-Indexed Evaluation
• • • • Exercise: 4 stars, standard (ceval_step__ceval_inf)
• • • • Exercise: 3 stars, standard, recommended (ceval__ceval_step)
• Volume 2: Programming Language Foundations
• • Program Equivalence
• • • Behavioral Equivalence
• • • • Simple Examples
• • • • • Exercise: 2 stars, standard (skip_right)
• • • • • Exercise: 2 stars, standard, recommended (TEST_false)
• • • • • Exercise: 3 stars, standard (swap_if_branches)
• • • • • Exercise: 2 stars, advanced, optional (WHILE_false_informal)
• • • • • Exercise: 2 stars, standard, optional (WHILE_true_nonterm_informal)
• • • • • Exercise: 2 stars, standard, recommended (WHILE_true)
• • • • • Exercise: 2 stars, standard, optional (seq_assoc)
• • • • • Exercise: 2 stars, standard, recommended (assign_aequiv)
• • • • • Exercise: 2 stars, standard (equiv_classes)
• • • Properties of Behavioral Equivalence
• • • • Behavioral Congruence Is a Congruence
• • • • • Exercise: 3 stars, standard, optional (CSeq_congruence)
• • • • • Exercise: 3 stars, standard (CIf_congruence)
• • • • • Exercise: 3 stars, advanced, optional (not_congr)
• • • Program Transformations
• • • • Soundness of Constant Folding
• • • • • Exercise: 3 stars, standard, optional (fold_bexp_Eq_informal)
• • • • • Exercise: 3 stars, standard (fold_constants_com_sound)
• • • • • Soundness of (0 + n) Elimination, Redux
• • • • • • Exercise: 4 stars, advanced, optional (optimize_0plus)
• • • Proving Inequivalence
• • • • Exercise: 4 stars, standard, optional (better_subst_equiv)
• • • • Exercise: 3 stars, standard (inequiv_exercise)
• • • Extended Exercise: Nondeterministic Imp
• • • • Exercise: 2 stars, standard (himp_ceval)
• • • • Exercise: 3 stars, standard (havoc_swap)
• • • • Exercise: 4 stars, standard, optional (havoc_copy)
• • • • Exercise: 4 stars, advanced (p1_p2_term)
• • • • Exercise: 4 stars, advanced (p1_p2_equiv)
• • • • Exercise: 4 stars, advanced (p3_p4_inequiv)
• • • • Exercise: 5 stars, advanced, optional (p5_p6_equiv)
• • • Additional Exercises
• • • • Exercise: 4 stars, standard, optional (for_while_equiv)
• • • • Exercise: 3 stars, standard, optional (swap_noninterfering_assignments)
• • • • Exercise: 4 stars, advanced, optional (capprox)
• • Hoare Logic, Part I
• • • Assertions
• • • • Exercise: 1 star, standard, optional (assertions)
• • • Hoare Triples
• • • • Exercise: 1 star, standard, optional (triples)
• • • • Exercise: 1 star, standard, optional (valid_triples)
• • • Proof Rules
• • • • Assignment
• • • • • Exercise: 2 stars, standard (hoare_asgn_examples)
• • • • • Exercise: 2 stars, standard, recommended (hoare_asgn_wrong)
• • • • • Exercise: 3 stars, advanced (hoare_asgn_fwd)
• • • • • Exercise: 2 stars, advanced, optional (hoare_asgn_fwd_exists)
• • • • Digression: The eapply Tactic
• • • • • Exercise: 2 stars, standard (hoare_asgn_examples_2)
• • • • Sequencing
• • • • • Exercise: 2 stars, standard, recommended (hoare_asgn_example4)
• • • • • Exercise: 3 stars, standard (swap_exercise)
• • • • • Exercise: 3 stars, standard (hoarestate1)
• • • • Conditionals
• • • • • Example
• • • • • • Exercise: 2 stars, standard (if_minus_plus)
• • • • • Exercise: One-sided conditionals
• • • • • • Exercise: 4 stars, standard (if1_hoare)
• • • • Loops
• • • • • Exercise: REPEAT
• • • • • • Exercise: 4 stars, advanced (hoare_repeat)
• • • Additional Exercises
• • • • Exercise: 3 stars, standard (hoare_havoc)
• • • • Exercise: 4 stars, standard, optional (assert_vs_assume)
• • Hoare Logic, Part II
• • • Decorated Programs
• • • • Example: Simple Conditionals
• • • • • Exercise: 2 stars, standard (if_minus_plus_reloaded)
• • • Finding Loop Invariants
• • • • Exercise: Slow Assignment
• • • • • Exercise: 2 stars, standard (slow_assignment)
• • • • Exercise: Slow Addition
• • • • • Exercise: 3 stars, standard, optional (add_slowly_decoration)
• • • • Example: Parity
• • • • • Exercise: 3 stars, standard, optional (parity_formal)
• • • • Exercise: Factorial
• • • • • Exercise: 3 stars, standard (factorial)
• • • • Exercise: Min
• • • • • Exercise: 3 stars, standard (Min_Hoare)
• • • • • Exercise: 3 stars, standard (two_loops)
• • • • Exercise: Power Series
• • • • • Exercise: 4 stars, standard, optional (dpow2_down)
• • • Weakest Preconditions (Optional)
• • • • Exercise: 1 star, standard, optional (wp)
• • • • Exercise: 3 stars, advanced, optional (is_wp_formal)
• • • • Exercise: 2 stars, advanced, optional (hoare_asgn_weakest)
• • • • Exercise: 2 stars, advanced, optional (hoare_havoc_weakest)
• • • Formal Decorated Programs (Advanced)
• • • • Further Exercises
• • • • • Exercise: 3 stars, advanced (slow_assignment_dec)
• • • • • Exercise: 4 stars, advanced (factorial_dec)
• • • • • Exercise: 4 stars, advanced, optional (fib_eqn)
• • • • • Exercise: 4 stars, advanced, optional (fib)
• • • • • Exercise: 5 stars, advanced, optional (improve_dcom)
• • • • • Exercise: 4 stars, advanced, optional (implement_dcom)
• • Hoare Logic as a Logic
• • • Properties
• • • • Exercise: 2 stars, standard (hoare_proof_sound)
• • • • Exercise: 1 star, standard (wp_is_precondition)
• • • • Exercise: 1 star, standard (wp_is_weakest)
• • • • Exercise: 5 stars, standard (hoare_proof_complete)
• • Small-step Operational Semantics
• • • A Toy Language
• • • • Exercise: 1 star, standard (test_step_2)
• • • Relations
• • • • Values
• • • • • Exercise: 3 stars, standard, recommended (redo_determinism)
• • • • Strong Progress and Normal Forms
• • • • • Exercise: 3 stars, standard, optional (value_not_same_as_normal_form1)
• • • • • Exercise: 2 stars, standard, optional (value_not_same_as_normal_form2)
• • • • • Exercise: 3 stars, standard, optional (value_not_same_as_normal_form3)
• • • • • Additional Exercises
• • • • • • Exercise: 1 star, standard (smallstep_bools)
• • • • • • Exercise: 3 stars, standard, optional (progress_bool)
• • • • • • Exercise: 2 stars, standard, optional (step_deterministic)
• • • • • • Exercise: 2 stars, standard (smallstep_bool_shortcut)
• • • • • • Exercise: 3 stars, standard, optional (properties_of_altered_step)
• • • Multi-Step Reduction
• • • • Examples
• • • • • Exercise: 1 star, standard, optional (test_multistep_2)
• • • • • Exercise: 1 star, standard, optional (test_multistep_3)
• • • • • Exercise: 2 stars, standard (test_multistep_4)
• • • • Normal Forms Again
• • • • • Exercise: 3 stars, standard, optional (normal_forms_unique)
• • • • • Exercise: 2 stars, standard (multistep_congr_2)
• • • • Equivalence of Big-Step and Small-Step
• • • • • Exercise: 3 stars, standard (eval__multistep)
• • • • • Exercise: 3 stars, advanced (eval__multistep_inf)
• • • • • Exercise: 3 stars, standard (step__eval)
• • • • • Exercise: 3 stars, standard (multistep__eval)
• • • • Additional Exercises
• • • • • Exercise: 3 stars, standard, optional (interp_tm)
• • • • • Exercise: 4 stars, standard (combined_properties)
• • • Concurrent Imp
• • • • Exercise: 3 stars, standard, optional (par_body_n__Sn)
• • • • Exercise: 3 stars, standard, optional (par_body_n)
• • • A Small-Step Stack Machine
• • • • Exercise: 3 stars, advanced (compiler_is_correct)
• • • Aside: A normalize Tactic
• • • • Exercise: 1 star, standard (normalize_ex)
• • • • Exercise: 1 star, standard, optional (normalize_ex')
• • Type Systems
• • • Typed Arithmetic Expressions
• • • • Normal Forms and Values
• • • • • Exercise: 2 stars, standard (some_term_is_stuck)
• • • • • Exercise: 3 stars, standard (value_is_nf)
• • • • • Exercise: 3 stars, standard, optional (step_deterministic)
• • • • Typing
• • • • • Exercise: 1 star, standard, optional (scc_hastype_nat__hastype_nat)
• • • • Progress
• • • • • Exercise: 3 stars, standard (finish_progress)
• • • • • Exercise: 3 stars, advanced (finish_progress_informal)
• • • • Type Preservation
• • • • • Exercise: 2 stars, standard (finish_preservation)
• • • • • Exercise: 3 stars, advanced (finish_preservation_informal)
• • • • • Exercise: 3 stars, standard (preservation_alternate_proof)
• • • • Additional Exercises
• • • • • Exercise: 2 stars, standard, recommended (subject_expansion)
• • • • • Exercise: 2 stars, standard (variation1)
• • • • • Exercise: 2 stars, standard (variation2)
• • • • • Exercise: 2 stars, standard, optional (variation3)
• • • • • Exercise: 2 stars, standard, optional (variation4)
• • • • • Exercise: 2 stars, standard, optional (variation5)
• • • • • Exercise: 2 stars, standard, optional (variation6)
• • • • • Exercise: 3 stars, standard, optional (more_variations)
• • • • • Exercise: 1 star, standard (remove_prdzro)
• • • • • Exercise: 4 stars, advanced (prog_pres_bigstep)
• • The Simply Typed Lambda-Calculus
• • • Operational Semantics
• • • • Substitution
• • • • • Exercise: 3 stars, standard (substi_correct)
• • • • Examples
• • • • • Exercise: 2 stars, standard (step_example5)
• • • Typing
• • • • Examples
• • • • • Exercise: 2 stars, standard, optional (typing_example_2_full)
• • • • • Exercise: 2 stars, standard (typing_example_3)
• • • • • Exercise: 3 stars, standard, optional (typing_nonexample_3)
• • Properties of STLC
• • • Progress
• • • • Exercise: 3 stars, advanced (progress_from_term_ind)
• • • Preservation
• • • • Free Occurrences
• • • • • Exercise: 1 star, standard (afi)
• • • • Substitution
• • • • • Exercise: 2 stars, standard, optional (typable_empty__closed)
• • • • Main Theorem
• • • • • Exercise: 2 stars, standard, recommended (subject_expansion_stlc)
• • • Type Soundness
• • • • Exercise: 2 stars, standard, optional (type_soundness)
• • • Uniqueness of Types
• • • • Exercise: 3 stars, standard (unique_types)
• • • Additional Exercises
• • • • Exercise: 1 star, standard (progress_preservation_statement)
• • • • Exercise: 2 stars, standard (stlc_variation1)
• • • • Exercise: 2 stars, standard (stlc_variation2)
• • • • Exercise: 2 stars, standard (stlc_variation3)
• • • • Exercise: 2 stars, standard, optional (stlc_variation4)
• • • • Exercise: 2 stars, standard, optional (stlc_variation5)
• • • • Exercise: 2 stars, standard, optional (stlc_variation6)
• • • • Exercise: 2 stars, standard, optional (stlc_variation7)
• • • • Exercise: STLC with Arithmetic
• • • • • Exercise: 5 stars, standard (stlc_arith)
• • More on the Simply Typed Lambda-Calculus
• • • Simple Extensions to STLC
• • • • General Recursion
• • • • • Exercise: 1 star, standard, optional (halve_fix)
• • • • • Exercise: 1 star, standard, optional (fact_steps)
• • • Exercise: Formalizing the Extensions
• • • • Exercise: 3 stars, standard (STLCE_definitions)
• • • • Examples
• • • • • Exercise: 3 stars, standard (STLCE_examples)
• • • • Properties of Typing
• • • • • Progress
• • • • • • Exercise: 3 stars, standard (STLCE_progress)
• • • • • Context Invariance
• • • • • • Exercise: 3 stars, standard (STLCE_context_invariance)
• • • • • Substitution
• • • • • • Exercise: 2 stars, standard (STLCE_subst_preserves_typing)
• • • • • Preservation
• • • • • • Exercise: 3 stars, standard (STLCE_preservation)
• • Subtyping
• • • Concepts
• • • • The Subtype Relation
• • • • • Records
• • • • • • Exercise: 2 stars, standard, recommended (arrow_sub_wrong)
• • • • Exercises
• • • • • Exercise: 1 star, standard, optional (subtype_instances_tf_1)
• • • • • Exercise: 2 stars, standard (subtype_order)
• • • • • Exercise: 1 star, standard (subtype_instances_tf_2)
• • • • • Exercise: 1 star, standard (subtype_concepts_tf)
• • • • • Exercise: 2 stars, standard (proper_subtypes)
• • • • • Exercise: 2 stars, standard (small_large_1)
• • • • • Exercise: 2 stars, standard (small_large_2)
• • • • • Exercise: 2 stars, standard, optional (small_large_3)
• • • • • Exercise: 2 stars, standard (small_large_4)
• • • • • Exercise: 2 stars, standard (smallest_1)
• • • • • Exercise: 2 stars, standard (smallest_2)
• • • • • Exercise: 3 stars, standard, optional (count_supertypes)
• • • • • Exercise: 2 stars, standard (pair_permutation)
• • • Formal Definitions
• • • • Subtyping
• • • • • Exercise: 2 stars, standard, optional (subtyping_judgements)
• • • • • Exercise: 1 star, standard, optional (subtyping_example_1)
• • • • • Exercise: 1 star, standard, optional (subtyping_example_2)
• • • • Typing
• • • • • Exercise: 1 star, standard, optional (typing_example_0)
• • • • • Exercise: 2 stars, standard, optional (typing_example_1)
• • • • • Exercise: 2 stars, standard, optional (typing_example_2)
• • • Properties
• • • • Inversion Lemmas for Subtyping
• • • • • Exercise: 2 stars, standard, optional (sub_inversion_Bool)
• • • • • Exercise: 3 stars, standard (sub_inversion_arrow)
• • • • Canonical Forms
• • • • • Exercise: 3 stars, standard, optional (canonical_forms_of_arrow_types)
• • • • Exercises
• • • • • Exercise: 2 stars, standard (variations)
• • • Exercise: Adding Products
• • • • Exercise: 5 stars, standard (products)
• • A Typechecker for STLC
• • • Exercises
• • • • Exercise: 5 stars, standard (typechecker_extensions)
• • • • Exercise: 5 stars, standard, optional (stlc_step_function)
• • • • Exercise: 5 stars, standard, optional (stlc_impl)
• • Adding Records to STLC
• • • Formalizing Records
• • • • Examples
• • • • • Exercise: 2 stars, standard (examples)
• • Typing Mutable References
• • • Pragmatics
• • • • Objects
• • • • • Exercise: 1 star, standard, optional (store_draw)
• • • • References to Compound Types
• • • • • Exercise: 2 stars, standard, recommended (compact_update)
• • • • Garbage Collection
• • • • • Exercise: 2 stars, standard (type_safety_violation)
• • • Typing
• • • • Store typings
• • • • • Exercise: 2 stars, standard (cyclic_store)
• • • Properties
• • • • Well-Typed Stores
• • • • • Exercise: 2 stars, standard (store_not_unique)
• • • • Preservation!
• • • • • Exercise: 3 stars, standard (preservation_informal)
• • • References and Nontermination
• • • • Exercise: 4 stars, standard (factorial_ref)
• • • Additional Exercises
• • • • Exercise: 5 stars, standard, optional (garbage_collector)
• • Subtyping with Records
• • • Subtyping
• • • • Examples
• • • • • Exercise: 2 stars, standard (subtyping_example_1)
• • • • • Exercise: 1 star, standard (subtyping_example_2)
• • • • • Exercise: 1 star, standard (subtyping_example_3)
• • • • • Exercise: 2 stars, standard (subtyping_example_4)
• • • • Properties of Subtyping
• • • • • Field Lookup
• • • • • • Exercise: 3 stars, standard (rcd_types_match_informal)
• • • • • Inversion Lemmas
• • • • • • Exercise: 3 stars, standard, optional (sub_inversion_arrow)
• • • Typing
• • • • Typing Examples
• • • • • Exercise: 1 star, standard (typing_example_0)
• • • • • Exercise: 2 stars, standard (typing_example_1)
• • • • • Exercise: 2 stars, standard, optional (typing_example_2)
• • • • Properties of Typing
• • • • • Progress
• • • • • • Exercise: 3 stars, standard (canonical_forms_of_arrow_types)
• • Normalization of STLC
• • • Exercise: 2 stars, standard (norm_fail)
• • • Exercise: 5 stars, standard, recommended (norm)
• • Theory and Practice of Automation in Coq Proofs
• • • Example Proofs using Automation
• • • • Determinism
• • • • Preservation for STLC
• • • • Progress for STLC
• • • • BigStep and SmallStep
• • • • Subtyping
• Volume 3: Verified Functional Algorithms
• • Basic Techniques for Comparisons and Permutations
• • • Permutations
• • • • • Exercise: 2 stars, standard (Permutation_properties)
• • • • • Exercise: 3 stars, standard (permut_example)
• • • • • Exercise: 2 stars, standard (not_a_permutation)
• • • An Inversion Tactic
• • • • • Exercise: 3 stars, standard (Forall_perm)
• • Insertion Sort
• • • Proof of Correctness
• • • • • Exercise: 3 stars, standard (insert_sorted)
• • • • • Exercise: 2 stars, standard (sort_sorted)
• • • • • Exercise: 3 stars, standard (insert_perm)
• • • • • Exercise: 3 stars, standard (sort_perm)
• • • • • Exercise: 1 star, standard (insertion_sort_correct)
• • • Validating the Specification (Advanced)
• • • • • Exercise: 4 stars, advanced (sorted_sorted')
• • • • • Exercise: 3 stars, advanced (sorted'_sorted)
• • • Proving Correctness from the Alternative Spec (Optional)
• • • • • Exercise: 5 stars, standard, optional (insert_sorted')
• • Insertion Sort Verified With Multisets
• • • Multisets
• • • • • Exercise: 1 star, standard (union_assoc)
• • • • • Exercise: 1 star, standard (union_comm)
• • • • • Exercise: 2 stars, standard (union_swap)
• • • Verification of Insertion Sort
• • • • • Exercise: 3 stars, standard (insert_contents)
• • • • • Exercise: 2 stars, standard (sort_contents)
• • • • • Exercise: 1 star, standard (insertion_sort_correct)
• • • • • Exercise: 1 star, standard (permutations_vs_multiset)
• • • Equivalence of Permutation and Multiset Specifications
• • • • The Forward Direction
• • • • • Exercise: 3 stars, standard (perm_contents)
• • • • The Backward Direction (Advanced)
• • • • • Exercise: 2 stars, advanced (contents_nil_inv)
• • • • • Exercise: 3 stars, advanced (contents_cons_inv)
• • • • • Exercise: 2 stars, advanced (contents_insert_other)
• • • • • Exercise: 3 stars, advanced (contents_perm)
• • • • The Main Theorem
• • • • • Exercise: 1 star, standard (same_contents_iff_perm)
• • • • • Exercise: 2 stars, standard (sort_specifications_equivalent)
• • Insertion Sort With Bags
• • • • • Exercise: 2 stars, standard (bag_eqv_properties)
• • • Correctness
• • • • • Exercise: 3 stars, standard (insert_bag)
• • • • • Exercise: 2 stars, standard (sort_bag)
• • • • • Exercise: 1 star, standard (permutations_vs_multiset)
• • • Permutations and Multisets
• • • • • Exercise: 3 stars, standard (perm_bag)
• • • • • Exercise: 2 stars, advanced (bag_nil_inv)
• • • • • Exercise: 3 stars, advanced (bag_cons_inv)
• • • • • Exercise: 2 stars, advanced (count_insert_other)
• • • • • Exercise: 3 stars, advanced (bag_perm)
• • Selection Sort
• • • Proof of Correctness
• • • • • Exercise: 2 stars, standard (select_perm)
• • • • • Exercise: 1 star, standard (select_rest_length)
• • • • • Exercise: 3 stars, standard (selsort_perm)
• • • • • Exercise: 1 star, standard (selection_sort_perm)
• • • • • Exercise: 2 stars, standard (select_fst_leq)
• • • • • Exercise: 1 star, standard (le_all__le_one)
• • • • • Exercise: 2 stars, standard (select_smallest)
• • • • • Exercise: 2 stars, standard (select_in)
• • • • • Exercise: 3 stars, standard (cons_of_small_maintains_sort)
• • • • • Exercise: 2 stars, standard (selsort_sorted)
• • • • • Exercise: 1 star, standard (selection_sort_sorted)
• • • • • Exercise: 1 star, standard (selection_sort_is_correct)
• • • Recursive Functions That are Not Structurally Recursive
• • • • • Exercise: 1 star, standard (selsort'_perm)
• • • • • Exercise: 1 star, standard (cons_of_small_maintains_sort')
• • • • • Exercise: 1 star, standard (selsort'_sorted)
• • • • • Exercise: 1 star, standard (selsort'_is_correct)
• • • Selection Sort with Multisets (Optional)
• • • • • Exercise: 3 stars, standard, optional (select_contents)
• • • • • Exercise: 3 stars, standard, optional (selection_sort_contents)
• • • • • Exercise: 2 stars, standard, optional (sorted_iff_sorted)
• • • • • Exercise: 1 star, standard, optional (selection_sort_correct')
• • Merge Sort, With Specification and Proof of Correctness
• • • • Split and its properties
• • • • • Exercise: 3 stars, standard (split_perm)
• • • • Correctness: Sortedness
• • • • • Exercise: 2 stars, standard (sorted_merge1)
• • • • • Exercise: 4 stars, standard (sorted_merge)
• • • • • Exercise: 2 stars, standard (mergesort_sorts)
• • • • Correctness: Permutation
• • • • • Exercise: 3 stars, advanced (merge_perm)
• • • • • Exercise: 3 stars, advanced (mergesort_perm)
• • Total and Partial Maps
• • • Total Maps
• • • • • Exercise: 1 star, standard (t_apply_empty)
• • • • • Exercise: 1 star, standard (t_update_eq)
• • • • • Exercise: 1 star, standard (t_update_neq)
• • • • • Exercise: 1 star, standard (t_update_shadow)
• • • • • Exercise: 1 star, standard (t_update_same)
• • • • • Exercise: 1 star, standard (t_update_permute)
• • Binary Search Trees
• • • BST Invariant
• • • • • Exercise: 1 star, standard (empty_tree_BST)
• • • • • Exercise: 3 stars, standard (insert_BST)
• • • Correctness of BST Operations
• • • • • Exercise: 3 stars, standard, optional (bound_correct)
• • • • • Exercise: 1 star, standard, optional (bound_default)
• • • BSTs vs. Higher-order Functions (Optional)
• • • • • Exercise: 2 stars, standard, optional (lookup_insert_shadow)
• • • • • Exercise: 2 stars, standard, optional (lookup_insert_same)
• • • • • Exercise: 2 stars, standard, optional (lookup_insert_permute)
• • • • • Exercise: 2 stars, standard, optional (direct_equalities_break)
• • • Converting a BST to a List
• • • • Part 1: Same Bindings
• • • • • Exercise: 3 stars, standard (elements_complete)
• • • • • Exercise: 2 stars, standard (elements_preserves_forall)
• • • • • Exercise: 2 stars, standard (elements_preserves_relation)
• • • • • Exercise: 4 stars, standard (elements_correct)
• • • • • Exercise: 2 stars, advanced (elements_complete_inverse)
• • • • • Exercise: 4 stars, advanced (elements_correct_inverse)
• • • • Part 2: Sorted (Advanced)
• • • • • Exercise: 3 stars, advanced (sorted_app)
• • • • • Exercise: 4 stars, advanced (sorted_elements)
• • • • Part 3: No Duplicates (Advanced and Optional)
• • • • • Exercise: 3 stars, advanced, optional (NoDup_append)
• • • • • Exercise: 4 stars, advanced, optional (elements_nodup_keys)
• • • A Faster [elements] Implementation
• • • • • Exercise: 3 stars, standard (fast_elements_eq_elements)
• • • An Algebraic Specification of [elements]
• • • • • Exercise: 3 stars, standard, optional (kvs_insert_split)
• • • • • Exercise: 3 stars, standard, optional (kvs_insert_elements)
• • • Model-based Specifications
• • • • • Exercise: 2 stars, standard, optional (in_fst)
• • • • • Exercise: 2 stars, standard, optional (in_map_of_list)
• • • • • Exercise: 2 stars, standard, optional (not_in_map_of_list)
• • • • • Exercise: 3 stars, standard, optional (bound_relate)
• • • • • Exercise: 3 stars, standard, optional (lookup_relate)
• • • • • Exercise: 3 stars, standard, optional (insert_relate)
• • • An Alternative Abstraction Relation (Optional, Advanced)
• • • • • Exercise: 2 stars, standard, optional (union_collapse)
• • • • • Exercise: 3 stars, standard, optional (union_update)
• • • • • Exercise: 3 stars, advanced, optional (map_of_tree_prop)
• • • • • Exercise: 3 stars, advanced, optional (bound_relate')
• • • • • Exercise: 3 stars, advanced, optional (lookup_relate')
• • • • • Exercise: 4 stars, advanced, optional (insert_relate')
• • • • • Exercise: 3 stars, advanced, optional (map_of_list_app)
• • • • • Exercise: 4 stars, advanced, optional (elements_relate')
• • Abstract Data Types
• • • Implementing [Table] with Functions
• • • • • Exercise: 2 stars, standard, optional (NatFunTableExamples)
• • • Implementing [Table] with Lists
• • • • • Exercise: 3 stars, standard (lists_table)
• • • Tables with an [elements] Operation
• • • • A Revised [ETable]
• • • Encapsulation with the Coq Module System (Advanced)
• • • • • Exercise: 4 stars, advanced, optional (elements_spec)
• • • Model-based Specification
• • • • • Exercise: 4 stars, standard (list_etable_abs)
• • • • • Exercise: 3 stars, standard, optional (TreeTableModel)
• • • • • Exercise: 2 stars, advanced, optional (TreeTableModel')
• • • Another ADT: Queue
• • • • • Exercise: 3 stars, standard (list_queue)
• • • • • Exercise: 3 stars, standard (two_list_queue)
• • • Representation Invariants and Subset Types
• • • • Example: Vectors
• • • • • Exercise: 1 star, standard (a_vector)
• • • • • Exercise: 2 stars, standard (vector_cons_correct)
• • • • • Exercise: 2 stars, standard (vector_app_correct)
• • • • Using Subset Types to Enforce the BST Invariant
• • • • • Exercise: 4 stars, advanced (ListsETable)
• • Running Coq Programs in OCaml
• • • Insertion Sort, Extracted
• • • • • Exercise: 3 stars, standard (sort_int_correct)
• • • Binary Search Trees, Extracted
• • • • • Exercise: 1 star, standard (lookup_insert_eq)
• • • • • Exercise: 2 stars, standard (lookup_insert_neq)
• • • • • Exercise: 4 stars, standard, optional (int_elements)
• • Red-Black Trees
• • • The BST Invariant
• • • • • Exercise: 2 stars, standard (balanceP)
• • • • • Exercise: 2 stars, standard (insP)
• • • • • Exercise: 3 stars, standard (ins_BST)
• • • • • Exercise: 2 stars, standard (insert_BST)
• • • Verification
• • • • • Exercise: 4 stars, standard (balance_lookup)
• • • • • Exercise: 3 stars, standard (lookup_ins_eq)
• • • • • Exercise: 3 stars, standard (lookup_ins_neq)
• • • • • Exercise: 2 stars, standard (lookup_insert)
• • • Efficiency
• • • • • Exercise: 1 star, standard (RB_blacken_parent)
• • • • • Exercise: 4 stars, standard (ins_RB)
• • • • • Exercise: 1 star, standard (RB_blacken_root)
• • • • • Exercise: 1 star, standard (insert_RB)
• • • • • Exercise: 4 stars, advanced (redblack_bound)
• • Number Representations and Efficient Lookup Tables
• • • Efficient Positive Numbers
• • • • • Exercise: 2 stars, standard (succ_correct)
• • • • • Exercise: 3 stars, standard (addc_correct)
• • • • • Exercise: 5 stars, standard (compare_correct)
• • • • From [NNlogN] to [NlogNlogN]
• • • Tries: Efficient Lookup Tables on Positive Binary Numbers
• • • • From [NlogNlogN] to [N*logN]
• • • • • Exercise: 2 stars, standard (successor_of_Z_constant_time)
• • • Proving the Correctness of Trie Tables
• • • • Lemmas About the Relation Between [lookup] and [insert]
• • • • • Exercise: 1 star, standard (look_leaf)
• • • • • Exercise: 2 stars, standard (look_ins_same)
• • • • • Exercise: 3 stars, standard (look_ins_same)
• • • • Bijection Between [positive] and [nat].
• • • • • Exercise: 2 stars, standard (pos2nat_bijective)
• • • • Proving That Tries are a "Table" ADT.
• • • • • Exercise: 2 stars, standard (is_trie)
• • • • • Exercise: 2 stars, standard (empty_relate)
• • • • • Exercise: 2 stars, standard (lookup_relate)
• • • • • Exercise: 3 stars, standard (insert_relate)
• • • • Sanity Check
• • Priority Queues
• • • Implementation
• • • • Some Preliminaries
• • • • • Exercise: 3 stars, standard (select_perm_and_friends)
• • • • The Program
• • • Predicates on Priority Queues
• • • • Characterizations of the Operations on Queues
• • • • • Exercise: 2 stars, standard (simple_priq_proofs)
• • Binomial Queues
• • • Proof of Algorithm Correctness
• • • • Various Functions Preserve the Representation Invariant
• • • • • Exercise: 1 star, standard (empty_priq)
• • • • • Exercise: 2 stars, standard (smash_valid)
• • • • • Exercise: 3 stars, standard (carry_valid)
• • • • • Exercise: 2 stars, standard, optional (insert_valid)
• • • • • Exercise: 3 stars, standard, optional (join_valid)
• • • • • Exercise: 5 stars, standard, optional (delete_max_Some_priq)
• • • • The Abstraction Relation
• • • • • Exercise: 3 stars, standard (priqueue_elems)
• • • • Sanity Checks on the Abstraction Relation
• • • • • Exercise: 2 stars, standard (tree_elems_ext)
• • • • • Exercise: 2 stars, standard (tree_perm)
• • • • • Exercise: 2 stars, standard (priqueue_elems_ext)
• • • • • Exercise: 2 stars, standard (abs_perm)
• • • • • Exercise: 2 stars, standard (can_relate)
• • • • Various Functions Preserve the Abstraction Relation
• • • • • Exercise: 1 star, standard (empty_relate)
• • • • • Exercise: 3 stars, standard (smash_elems)
• • • • Optional Exercises
• • • • • Exercise: 4 stars, standard, optional (carry_elems)
• • • • • Exercise: 2 stars, standard, optional (insert_elems)
• • • • • Exercise: 4 stars, standard, optional (join_elems)
• • • • • Exercise: 2 stars, standard, optional (merge_relate)
• • • • • Exercise: 5 stars, standard, optional (delete_max_None_relate)
• • • • • Exercise: 5 stars, standard, optional (delete_max_Some_relate)
• • • Measurement.
• • • • • Exercise: 5 stars, standard, optional (binom_measurement)
• • Programming with Decision Procedures
• • • Using [sumbool] to Characterize Decision Procedures
• • • • [sumbool] in the Coq Standard Library
• • • • • Exercise: 2 stars, standard (insert_sorted_le_dec)
• • • Opacity of [Qed]
• • • • • Exercise: 2 stars, standard (list_nat_in)
• • Graph Coloring
• • • Lemmas About Sets and Maps
• • • • S.remove and S.elements
• • • • • Exercise: 3 stars, standard (Sremove_elements)
• • • • Lists of (key,value) Pairs
• • • • • Exercise: 2 stars, standard (InA_map_fst_key)
• • • • • Exercise: 3 stars, standard (Sorted_lt_key)
• • • • Cardinality
• • • • • Exercise: 4 stars, standard (cardinal_map)
• • • • • Exercise: 4 stars, standard (Sremove_cardinal_less)
• • • • • Exercise: 4 stars, standard (Mremove_elements)
• • • • • Exercise: 3 stars, standard (Mremove_cardinal_less)
• • • • • Exercise: 2 stars, standard (two_little_lemmas)
• • • • • Exercise: 3 stars, standard (Sin_domain)
• • • Now Begins the Graph Coloring Program
• • • • Some Proofs in Support of Termination
• • • • • Exercise: 3 stars, standard (subset_nodes_sub)
• • • • • Exercise: 3 stars, standard (select_terminates)
• • • • The Rest of the Algorithm
• • • Proof of Correctness of the Algorithm.
• • • • • Exercise: 2 stars, standard (adj_ext)
• • • • • Exercise: 3 stars, standard (in_colors_of_1)
• • • • • Exercise: 4 stars, standard (color_correct)
• Volume 4: QuickChick: Property-Based Testing in Coq
• Volume 5: Verifiable C
• • Introduction to Verifiable C
• • Linked lists in Verifiable C
• • Stack ADT implemented by linked lists
• • • Specification of linked lists
• • • • Exercise: 1 star, standard (stack_listrep_properties)
• • • Specification of stack data structure
• • • • Exercise: 1 star, standard (stack_properties)
• • • Proofs of the function bodies
• • • • Exercise: 2 stars, standard (body_pop)
• • • • Exercise: 2 stars, standard (body_push)
• • • • Exercise: 2 stars, standard (body_newstack)
• • A client of the stack functions
• • • Proofs with integers
• • • • Exercise: 2 stars, standard (Zinduction)
• • • • A theorem about the nth triangular number
• • • • • Exercise: 2 stars, standard (add_list_decreasing)
• • • Proofs of the stack-client function-bodies
• • • • Exercise: 3 stars, standard (body_push_increasing)
• • • • Exercise: 2 stars, standard (add_list_lemmas)
• • • • Exercise: 2 stars, standard (add_list_sublist_bounds)
• • • • Exercise: 3 stars, standard (add_another)
• • • • Exercise: 3 stars, standard (body_pop_and_add)
• • • • Exercise: 3 stars, standard (body_main)
• • List segments
• • • List segments.
• • • • Exercise: 1 star, standard (singleton_lseg)
• • • • Exercise: 1 star, standard (lseg_lseg)
• • • • Exercise: 1 star, standard (lseg_list)
• • • Proof of the append function
• • • • Exercise: 1 star, standard (listrep_null)
• • • • Exercise: 1 star, standard (listrep_nonnull)
• • • • Exercise: 3 stars, standard (body_append)
• • • Additional exercises: more proofs about list segments
• • • • Exercise: 1 star, standard: (lseg2listrep)
• • • • Exercise: 1 star, standard: (listrep2lseg)
• • • • Exercise: 2 stars, standard: (lseg_lseg_inv)
• • • • Exercise: 2 stars, standard: (loopy_lseg_no_connection)
• • • Additional exercises: loop-free list segments
• • • • Exercise: 2 stars, standard, optional (nt_lseg)
• • • • Exercise: 2 stars, standard, optional (singleton_nt_lseg')
• • • • Exercise: 2 stars, standard, optional (nt_lseg_nt_lseg)
• • • • Exercise: 2 stars, standard, optional (nt_lseg_list)
• • • • Exercise: 3 stars, standard, optional (body_append_alter1)
• • Magic wand, partial data structure
• • • Separating Implication
• • • • Exercise: 2 stars, standard: (wand_derives)
• • • • Exercise: 2 stars, standard: (wand_frame_ver)
• • • • Exercise: 3 stars, standard: (emp_wand_emp)
• • • List segments by magic wand
• • • • Exercise: 2 stars, standard: (singleton_wlseg)
• • • • Exercise: 2 stars, standard: (wlseg_list)
• • • Proof of the append function by wlseg
• • • • Exercise: 3 stars, standard: (body_append_alter2)
• • • Case study: list segments for linked list box
• • • • Exercise: 1 star, standard: (emp_lbseg)
• • • • Exercise: 2 stars, standard: (lbseg_lbseg)
• • • • Exercise: 2 stars, standard: (listbox_lbseg)
• • String functions
• • • Proof of the strlen function
• • • • Exercise: 2 stars, standard (body_strlen)
• • • Proof of the strcpy function
• • • • Exercise: 2 stars, standard (strcpy_then_clause)
• • • • Exercise: 2 stars, standard (strcpy_else_clause)
• • • • data_at is not injective!
• • • • • Exercise: 3 stars, standard (body_strcpy)
• • • • • Exercise: 3 stars, standard (example_call_strcpy)
• • • • • Exercise: 4 stars, standard, optional (body_strcmp)
• • Functional model of hash tables
• • • A functional model
• • • • Exercise: 2 stars, standard (hashfun_inrange)
• • • • Exercise: 1 star, standard (hashfun_get_unfold)
• • • • Exercise: 2 stars, standard (Zlength_hashtable_incr)
• • • • Exercise: 3 stars, standard (hashfun_snoc)
• • • Functional model satisfies the high-level specification
• • • • A "reference" implementation of COUNT_TABLE
• • • • • Exercise: 2 stars, standard (FunTable)
• • • • Demonstration that hash tables implement COUNT_TABLE
• • • • • Exercise: 3 stars, standard (IntHashTable)
• • Correctness proof of hash.c
• • • Function specifications
• • • • Data structures for hash table
• • • • • Exercise: 1 star, standard (listcell_fold)
• • • • • Exercise: 2 stars, standard (listrep_hints)
• • • • • Exercise: 2 stars, standard (hashtable_rep_hints)
• • • Proofs of the functions hash, copy_string, new_cell
• • • • Exercise: 3 stars, standard (body_hash)
• • • • Exercise: 3 stars, standard (body_copy_string)
• • • • Exercise: 3 stars, standard (body_new_cell)
• • • Proof of the new_table function
• • • • Auxiliary lemmas about data-structure predicates
• • • • • Exercise: 2 stars, standard (iter_sepcon_hints)
• • • • • Exercise: 2 stars, standard (iter_sepcon_split3)
• • • • • Exercise: 3 stars, standard (body_new_table)
• • • Proof of the get function
• • • • Exercise: 2 stars, standard (listrep_traverse)
• • • • Exercise: 3 stars, standard (body_get)
• • • Proof of the incr_list function
• • • • Exercise: 3 stars, standard (listboxrep_traverse)
• • • • Exercise: 4 stars, standard (body_incr_list)
• • • Proof of the incr function
• • • • Exercise: 4 stars, standard (body_incr)
• Volume 6: Separation Logic Foundations
• • Basic Proofs in Separation Logic
• • • A First Taste
• • • • A Function with a Return Value
• • • • • Exercise: 1 star, standard, especially useful (triple_quadruple)
• • • • • Exercise: 2 stars, standard, especially useful (triple_inplace_double)
• • • Separation Logic Operators
• • • • Transfer from one Reference to Another
• • • • • Exercise: 1 star, standard, especially useful (triple_transfer)
• • • • • Exercise: 1 star, standard, especially useful (triple_transfer_aliased)
• • • • Allocation of a Reference with Greater Contents
• • • • • Exercise: 2 stars, standard, especially useful (triple_ref_greater_abstract)
• • • • Combined Reading and Freeing of a Reference
• • • • • Exercise: 2 stars, standard, especially useful (triple_get_and_free)
• • • • Nondeterminism: Specifying Random Output Values
• • • • • Exercise: 2 stars, standard, optional (triple_two_dice)
• • • Recursive Functions
• • • • A Recursive Function with State
• • • • • Exercise: 2 stars, standard, especially useful (triple_repeat_incr)
• • • • Trying to Prove Incorrect Specifications
• • • • • Exercise: 2 stars, standard, optional (triple_repeat_incr')
• • • • A Recursive Function Involving two References
• • • • • Exercise: 2 stars, standard, especially useful (triple_step_transfer)
• • Representation Predicates
• • • First Pass
• • • • Length Function for Lists
• • • • • Exercise: 3 stars, standard, especially useful (triple_mlength)
• • • • Alternative Length Function for Lists
• • • • • Exercise: 3 stars, standard, especially useful (triple_mlength')
• • • • Free Function for Lists
• • • • • Exercise: 3 stars, standard, especially useful (Triple_mfree)
• • • • In-Place Reversal Function for Lists
• • • • • Exercise: 5 stars, standard, optional (triple_mrev)
• • • More Details
• • • • Sized Stack
• • • • • Exercise: 3 stars, standard, especially useful (triple_push)
• • • • • Exercise: 4 stars, standard, especially useful (triple_pop)
• • • • • Exercise: 2 stars, standard, optional (triple_top)
• • • • Additional Tooling for [MTree]
• • • • • Exercise: 2 stars, standard, optional (triple_mnode')
• • • • Tree Copy
• • • • • Exercise: 3 stars, standard, optional (triple_tree_copy)
• • • • Computing the Sum of the Items in a Tree
• • • • • Exercise: 4 stars, standard, optional (triple_mtreesum)
• • • • Verification of a Counter Function with Local State
• • • • • Exercise: 4 stars, standard, especially useful (triple_apply_counter_abstract)
• • • • • Exercise: 2 stars, standard, optional (triple_test_counter)
• • • Optional Material
• • • • Specification of an Iterator on Mutable Lists
• • • • • Exercise: 5 stars, standard, especially useful (triple_miter)
• • • • Computing the Length of a Mutable List using an Iterator
• • • • • Exercise: 4 stars, standard, especially useful (triple_mlength_using_miter)
• • • • A Factorial Function in Continuation-Passing Style
• • • • • Exercise: 4 stars, standard, optional (triple_cps_facto_aux)
• • • • • Exercise: 2 stars, standard, optional (triple_cps_facto)
• • • • An In-Place Concatenation Function in Continuation-Passing Style
• • • • • Exercise: 5 stars, standard, optional (triple_cps_append_aux)
• • • • • Exercise: 3 stars, standard, optional (triple_cps_append)
• • Heap Entailment
• • • First Pass
• • • • Definition of Entailment
• • • • • Exercise: 1 star, standard, especially useful (himpl_antisym)
• • • • Entailment for Postconditions
• • • • • Exercise: 1 star, standard, especially useful (qimpl_antisym)
• • • • Introduction and Elimination Rules w.r.t. Entailments
• • • • • Exercise: 2 stars, standard, especially useful (himpl_hstar_hpure_r).
• • • • • Exercise: 2 stars, standard, especially useful (himpl_hstar_hpure_l).
• • • • • Exercise: 2 stars, standard, especially useful (himpl_hexists_r).
• • • • • Exercise: 2 stars, standard, especially useful (himpl_hexists_l).
• • • • Extracting Information from Heap Predicates
• • • • • Rules for Naming Heaps
• • • • • Exercise: 3 stars, standard, optional (hexists_named_eq)
• • • • Identifying True and False Entailments
• • • More Details
• • • • Proving Entailments by Hand
• • • • • Exercise: 3 stars, standard, optional (himpl_example_1)
• • • • • Exercise: 3 stars, standard, optional (himpl_example_2)
• • • • • Exercise: 3 stars, standard, optional (himpl_example_3)
• • • • The [xsimpl] Tactic
• • • • • [xsimpl] to Extract Pure Facts and Quantifiers in LHS
• • • • • [xsimpl] to Cancel Out Heap Predicates from LHS and RHS
• • • • • [xsimpl] to Instantiate Pure Facts and Quantifiers in RHS
• • • • • [xsimpl] on Entailments Between Postconditions
• • • • • Example of Entailment Proofs using [xpull] and [xsimpl]
• • • • The [xchange] Tactic
• • • • • Exercise: 2 stars, standard, especially useful (xchange_lemma)
• • • Optional Material
• • • • Proofs of Rules for Entailment
• • • • • Exercise: 1 star, standard, especially useful (himpl_frame_l)
• • • • • Exercise: 1 star, standard, especially useful (himpl_frame_r)
• • • • • Exercise: 1 star, standard, especially useful (himpl_frame_lr)
• • Structural Reasoning Rules
• • • First Pass
• • • • Derived Structural Rules
• • • • • Exercise: 1 star, standard, especially useful (triple_conseq_frame)
• • • • • Exercise: 1 star, standard, optional (triple_hpure')
• • • More Details
• • • • Proof of the Extraction Rules
• • • • • Exercise: 1 star, standard, especially useful (triple_hexists)
• • • • Rule for Naming Heaps
• • • • • Exercise: 1 star, standard, optional (triple_named_heap)
• • • Optional Material
• • • • Alternative Structural Rule for Existentials
• • • • • Exercise: 2 stars, standard, especially useful (triple_hexists2)
• • • • • Exercise: 2 stars, standard, especially useful (triple_hexists_of_triple_hexists2)
• • • • Equivalence Between Small-Step and Omni-Big-Step
• • • • • Exercise: 2 stars, standard, optional (seval_val_inv)
• • • • • Exercise: 2 stars, standard, especially useful (seval_terminates)
• • • • • Exercise: 3 stars, standard, especially useful (seval_safe)
• • • • • Exercise: 3 stars, standard, especially useful (seval_correct)
• • • • • Exercise: 5 stars, standard, especially useful (seval_seq)
• • • • • Exercise: 5 stars, standard, optional (seval_let)
• • • • Separation Logic Triples for Quasi-Deterministics Semantics
• • • • • Exercise: 2 stars, standard, especially useful (hoare_conseq)
• • • • • Exercise: 3 stars, standard, especially useful (btriple_frame)
• • Reasoning Rules for Term Constructs
• • • First Pass
• • • • Rules for Term Constructs
• • • • • Exercise: 2 stars, standard, especially useful (triple_seq)
• • • • • Exercise: 2 stars, standard, especially useful (triple_if_case)
• • • • • Exercise: 1 star, standard, especially useful (triple_val_minimal)
• • • • • Exercise: 2 stars, standard, especially useful (triple_val')
• • • • • Exercise: 4 stars, standard, especially useful (triple_let_val)
• • • • Rules for Primitive Arithmetic Operations
• • • • • Exercise: 2 stars, standard, especially useful (triple_rand)
• • • • Rules for Primitive Heap-Manipulating Operations
• • • • • Exercise: 2 stars, standard, especially useful (triple_free')
• • • • • Exercise: 2 stars, standard, especially useful (triple_set)
• • • • Program Verification using the Reasoning Rules of Separation Logic
• • • • • Exercise: 4 stars, standard, especially useful (triple_succ_using_incr)
• • • More Details
• • • • Triple for Terms with Same Semantics
• • • • • Exercise: 1 star, standard, especially useful (eval_like_eta_expansion)
• • • • • Exercise: 4 stars, standard, optional (eval_like_eta_expansion)
• • • • • Exercise: 2 stars, standard, especially useful (eta_same_triples)
• • • • • Exercise: 3 stars, standard, optional (triple_trm_seq_assoc)
• • • • The Combined Let-Frame Rule
• • • • • Exercise: 3 stars, standard, especially useful (triple_let_frame)
• • • Optional Material
• • • • Alternative Specification Style for Pure Preconditions
• • • • • Exercise: 2 stars, standard, especially useful (triple_div_from_triple_div')
• • • • Alternative Specification Style for Result Values
• • • • • Exercise: 4 stars, standard, especially useful (triple_factorec)
• • The Magic Wand and Other Operators
• • • First Pass
• • • • Operator [hor]
• • • • • Exercise: 3 stars, standard, optional (hor_eq_hor')
• • • • • Exercise: 2 stars, standard, especially useful (hor_comm)
• • • • • Exercise: 4 stars, standard, especially useful (hor_comm)
• • • • Operator [hand]
• • • • • Exercise: 2 stars, standard, especially useful (hand_eq_hand')
• • • • • Exercise: 1 star, standard, especially useful (hand_comm)
• • • • Magic Wand: [hwand]
• • • • • Exercise: 2 stars, standard, especially useful (hwand_hpure_l)
• • • • • Exercise: 2 stars, standard, optional (himpl_hwand_hpure_lr)
• • • • • Exercise: 1 star, standard, especially useful (himpl_hwand_hstar_same_r)
• • • • • Exercise: 2 stars, standard, especially useful (hwand_cancel_part)
• • • • • Exercise: 3 stars, standard, optional (hwand_frame)
• • • • • Exercise: 3 stars, standard, optional (hwand_inv)
• • • • Magic Wand for Postconditions: [qwand]
• • • • • Exercise: 1 star, standard, especially useful (himpl_qwand_hstar_same_r)
• • • • • Exercise: 2 stars, standard, optional (qwand_cancel_part)
• • Semantics of Weakest Preconditions
• • • First Pass
• • • • • Exercise: 3 stars, standard, especially useful (wp_conseq_of_wp_ramified)
• • • • • Exercise: 3 stars, standard, especially useful (wp_frame_of_wp_ramified)
• • • • Reasoning Rules for Terms, in Weakest-Precondition Style
• • • • • Exercise: 1 star, standard, optional (wp_if')
• • • • • Rule For Function Applications
• • • More Details
• • • • Combined Structural Rule
• • • • • Exercise: 2 stars, standard, especially useful (wp_conseq_frame_trans)
• • • • • Exercise: 2 stars, standard, especially useful (wp_conseq_frame)
• • • Optional Material
• • • • Weakest Preconditions Derived from Triples, a First Route
• • • • • Exercise: 3 stars, standard, especially useful (wp_equiv_1)
• • • • Weakest Preconditions Derived From Triples, a Second Route
• • • • • Exercise: 4 stars, standard, optional (wp_equiv_2)
• • • • Characterizations of [wp]
• • • • • Exercise: 2 stars, standard, especially useful (wp_equiv_iff_wp_pre_and_wp_weakest)
• • • • Texan Triples
• • • • • Exercise: 3 stars, standard, especially useful (wp_incr)
• • Weakest Precondition Generator
• • • More Details
• • • • An Example Proof
• • • • • Exercise: 2 stars, standard, especially useful (triple_succ_using_incr_with_xlemmas)
• • • • Making Proof Scripts More Concise
• • • • • Exercise: 2 stars, standard, especially useful (triple_succ_using_incr_with_xtactics)
• • • Optional Material
• • • • Tactics [xconseq] and [xframe]
• • • • • Exercise: 1 star, standard, optional (xconseq_lemma)
• • • • • Exercise: 2 stars, standard, optional (xframe_lemma)