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.

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)
• • Tactic Library for Coq: A Gentle Introduction
• • • Tactics for Advanced Lemma Instantiation
• • • • Example of Instantiations
• • 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 Permutations and Ordering
• • • Permutations
• • • • Exercise: 2 stars (Permutation_properties)
• • • • Exercise: 3 stars (permut_example)
• • • • Exercise: 1 star (not_a_permutation)
• • • Summary: Comparisons and Permutations
• • • • Exercise: 2 stars (Forall_perm)
• • Insertion Sort
• • • Proof of Correctness
• • • • Exercise: 3 stars (insert_perm)
• • • • Exercise: 3 stars (sort_perm)
• • • • Exercise: 4 stars (insert_sorted)
• • • • Exercise: 2 stars (sort_sorted)
• • • Making Sure the Specification is Right
• • • • Exercise: 4 stars, optional (sorted_sorted')
• • • • Exercise: 3 stars, optional (sorted'_sorted)
• • • Proving Correctness from the Alternate Spec
• • • • Exercise: 3 stars, optional (Forall_nth)
• • • • Exercise: 4 stars, optional (insert_sorted')
• • • • Exercise: 4 stars, optional (sort_sorted')
• • Insertion Sort With Multisets
• • • Exercise: 1 star (union_assoc)
• • • Exercise: 1 star (union_comm)
• • • Correctness
• • • • Exercise: 3 stars (insert_contents)
• • • • Exercise: 3 stars (sort_contents)
• • • • Exercise: 1 star (permutations_vs_multiset)
• • • Permutations and Multisets
• • • • Exercise: 3 stars (perm_contents)
• • • • Exercise: 3 stars (delete_contents)
• • • • Exercise: 2 stars (contents_perm_aux)
• • • • Exercise: 2 stars (contents_in)
• • • • Exercise: 2 stars (in_perm_delete)
• • • • Exercise: 4 stars (contents_perm)
• • Selection Sort, With Specification and Proof of Correctness
• • • Proof of Correctness of Selection sort
• • • • Exercise: 3 stars (select_perm)
• • • • Exercise: 3 stars (selection_sort_perm)
• • • • Exercise: 3 stars (select_smallest)
• • • • Exercise: 3 stars (selection_sort_sorted)
• • • Recursive Functions That are Not Structurally Recursive
• • • • Exercise: 3 stars (selsort'_perm)
• • Binary Search Trees
• • • Proof of Correctness
• • • • Exercise: 2 stars (example_map)
• • • • Exercise: 3 stars (check_example_map)
• • • • Exercise: 3 stars (lookup_relate)
• • • • Exercise: 4 stars (insert_relate)
• • • Correctness Proof of the elements Function
• • • • Exercise: 3 stars (elements_relate_informal)
• • • • Exercise: 4 stars (not_elements_relate)
• • • Representation Invariants
• • • • Exercise: 3 stars, optional (elements_slow_elements)
• • • • Exercise: 3 stars, optional (slow_elements_range)
• • • • Auxiliary Lemmas About In and list2map
• • • • • Exercise: 3 stars, optional (elements_relate)
• • • Preservation of Representation Invariant
• • • • Exercise: 1 star (empty_tree_SearchTree)
• • • • Exercise: 3 stars (insert_SearchTree)
• • • Every Well-Formed Tree Does Actually Relate to an Abstraction
• • • • Exercise: 2 stars (can_relate)
• • • • Exercise: 2 stars (unrealistically_strong_can_relate)
• • • It Wasn't Really Luck, Actually
• • • • Exercise: 4 stars, optional (lookup_relateX)
• • Abstract Data Types
• • • Exercise: 3 stars (TreeTable_gso)
• • • A Brief Excursion into Dependent Types
• • • • Exercise: 3 stars (TreeTable2_gso)
• • • Exercise in Data Abstraction
• • • • Exercise: 4 stars, optional (listish_abstraction)
• • • • Exercise: 2 stars, optional (fib_time_complexity)
• • Running Coq programs in ML
• • • SearchTrees, Extracted
• • • • Trees, on int Instead of nat
• • • • • Exercise: 3 stars (lookup_relate)
• • • • • Exercise: 3 stars (insert_relate)
• • • • • Exercise: 1 star (unrealistically_strong_can_relate)
• • Implementation and Proof of Red-Black Trees
• • • The SearchTree Property
• • • • Exercise: 2 stars (ins_SearchTree)
• • • • Exercise: 2 stars (valid)
• • • • Exercise: 3 stars (lookup_relate)
• • • • Exercise: 4 stars (balance_relate)
• • • • Exercise: 3 stars (ins_relate)
• • • • Exercise: 4 stars, optional (elements)
• • • Proving Efficiency
• • • • Exercise: 4 stars (is_redblack_properties)
• • Number Representations and Efficient Lookup Tables
• • • Efficient Positive Numbers
• • • • Exercise: 2 stars (succ_correct)
• • • • Exercise: 3 stars (addc_correct)
• • • • Exercise: 5 stars (compare_correct)
• • • Tries: Efficient Lookup Tables on Positive Binary Numbers
• • • • From N*logN*logN to N*logN
• • • • • Exercise: 2 stars (successor_of_Z_constant_time)
• • • Proving the Correctness of Trie Tables
• • • • Lemmas About the Relation Between lookup and insert
• • • • • Exercise: 1 star (look_leaf)
• • • • • Exercise: 2 stars (look_ins_same)
• • • • • Exercise: 3 stars (look_ins_other)
• • • • Bijection Between positive and nat.
• • • • • Exercise: 2 stars (pos2nat_bijective)
• • • • Proving That Tries are a "Table" ADT.
• • • • • Exercise: 2 stars (is_trie)
• • • • • Exercise: 2 stars (empty_relate)
• • • • • Exercise: 2 stars (lookup_relate)
• • • • • Exercise: 3 stars (insert_relate)
• • • • Sanity Check
• • Priority Queues
• • • Implementation
• • • • Some Preliminaries
• • • • • Exercise: 3 stars (select_perm_and_friends)
• • • Predicates on Priority Queues
• • • • Characterizations of the Operations on Queues
• • • • • Exercise: 2 stars (simple_priq_proofs)
• • Binomial Queues
• • • Proof of Algorithm Correctness
• • • • Various Functions Preserve the Representation Invariant
• • • • • Exercise: 1 star (empty_priq)
• • • • • Exercise: 2 stars (smash_valid)
• • • • • Exercise: 3 stars (carry_valid)
• • • • • Exercise: 2 stars, optional (insert_valid)
• • • • • Exercise: 3 stars, optional (join_valid)
• • • • • Exercise: 5 stars, optional (delete_max_Some_priq)
• • • • The Abstraction Relation
• • • • • Exercise: 3 stars (priqueue_elems)
• • • • Sanity Checks on the Abstraction Relation
• • • • • Exercise: 2 stars (tree_elems_ext)
• • • • • Exercise: 2 stars (tree_perm)
• • • • • Exercise: 2 stars (priqueue_elems_ext)
• • • • • Exercise: 2 stars (abs_perm)
• • • • • Exercise: 2 stars (can_relate)
• • • • Various Functions Preserve the Abstraction Relation
• • • • • Exercise: 1 star (empty_relate)
• • • • • Exercise: 3 stars (smash_elems)
• • • • Optional Exercises
• • • • • Exercise: 4 stars, optional (carry_elems)
• • • • • Exercise: 2 stars, optional (insert_elems)
• • • • • Exercise: 4 stars, optional (join_elems)
• • • • • Exercise: 2 stars, optional (merge_relate)
• • • • • Exercise: 5 stars, optional (delete_max_None_relate)
• • • • • Exercise: 5 stars, optional (delete_max_Some_relate)
• • • Measurement.
• • • • Exercise: 5 stars, optional (binom_measurement)
• • Programming with Decision Procedures
• • • Using sumbool to Characterize Decision Procedures
• • • • sumbool in the Coq Standard Library
• • • • • Exercise: 2 stars (insert_sorted_le_dec)
• • • Decidability and Computability
• • • • Opacity of Qed
• • • • • Exercise: 2 stars (list_nat_in)
• • Graph Coloring
• • • Lemmas About Sets and Maps
• • • • S.remove and S.elements
• • • • • Exercise: 3 stars (Sremove_elements)
• • • • Lists of (key,value) Pairs
• • • • • Exercise: 2 stars (InA_map_fst_key)
• • • • • Exercise: 3 stars (Sorted_lt_key)
• • • • Cardinality
• • • • • Exercise: 4 stars (cardinal_map)
• • • • • Exercise: 4 stars (Sremove_cardinal_less)
• • • • • Exercise: 4 stars (Mremove_elements)
• • • • • Exercise: 3 stars (Mremove_cardinal_less)
• • • • • Exercise: 2 stars (two_little_lemmas)
• • • • • Exercise: 3 stars (Sin_domain)
• • • Now Begins the Graph Coloring Program
• • • • Some Proofs in Support of Termination
• • • • • Exercise: 3 stars (subset_nodes_sub)
• • • • • Exercise: 3 stars (select_terminates)
• • • Proof of Correctness of the Algorithm.
• • • • Exercise: 2 stars (adj_ext)
• • • • Exercise: 3 stars (in_colors_of_1)
• • • • Exercise: 4 stars (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)