Library PLF.Bib

• Bib: Bibliography
• Resources cited in this volume

Library PLF.Equiv

• Equiv: Program Equivalence
  • • Before You Get Started:
    • Advice for Working on Exercises:
• Behavioral Equivalence
  • Definitions
  • Simple Examples
    • • Exercise: 2 stars, standard (skip_right)
      • Exercise: 2 stars, standard, especially useful (if_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, especially useful (while_true)
      • Exercise: 2 stars, standard, optional (seq_assoc)
      • Exercise: 2 stars, standard, especially useful (assign_aequiv)
      • Exercise: 2 stars, standard (equiv_classes)
• Properties of Behavioral Equivalence
  • Behavioral Equivalence Is an Equivalence
  • Behavioral Equivalence Is a Congruence
    • • Exercise: 3 stars, standard, optional (CSeq_congruence)
      • Exercise: 3 stars, standard (CIf_congruence)
      • Exercise: 3 stars, advanced (not_congr)
• Program Transformations
  • The Constant-Folding Transformation
  • 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, standard, optional (optimize_0plus_var)
• 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: 3 stars, standard, optional (swap_noninterfering_assignments)
      • Exercise: 4 stars, standard, optional (for_while_equiv)
      • Exercise: 4 stars, advanced, optional (capprox)

Library PLF.Hoare

• Hoare: Hoare Logic, Part I
• Assertions
  • • • Exercise: 1 star, standard, optional (assertions)
  • Notations for Assertions
  • Example Assertions
  • Assertion Implication
• Hoare Triples, Informally
  • • • Exercise: 1 star, standard, optional (triples)
      • Exercise: 1 star, standard, optional (valid_triples)
• Hoare Triples, Formally
  • • • Exercise: 1 star, standard (hoare_post_true)
      • Exercise: 1 star, standard (hoare_pre_false)
• Proof Rules
  • Skip
  • Sequencing
  • Assignment
    • • Exercise: 2 stars, standard, optional (hoare_asgn_examples1)
      • Exercise: 2 stars, standard, optional (hoare_asgn_examples2)
      • Exercise: 2 stars, standard, especially useful (hoare_asgn_wrong)
      • Exercise: 3 stars, advanced (hoare_asgn_fwd)
      • Exercise: 2 stars, advanced, optional (hoare_asgn_fwd_exists)
  • Consequence
  • Automation
    • • Exercise: 2 stars, standard (hoare_asgn_examples_2)
  • Sequencing + Assignment
    • • Exercise: 2 stars, standard, especially useful (hoare_asgn_example4)
      • Exercise: 3 stars, standard (swap_exercise)
      • Exercise: 4 stars, advanced (invalid_triple)
  • Conditionals
    • Example
      • Exercise: 2 stars, standard (if_minus_plus)
    • Exercise: One-sided conditionals
      • Exercise: 2 stars, standard, especially useful (if1_ceval)
      • Exercise: 2 stars, standard (hoare_if1)
      • Exercise: 2 stars, standard (hoare_if1_good)
  • While Loops
    • Exercise: REPEAT
      • Exercise: 4 stars, advanced, optional (hoare_repeat)
• Summary
• Additional Exercises
  • Havoc
    • • Exercise: 3 stars, advanced (hoare_havoc)
      • Exercise: 3 stars, advanced (havoc_post)
  • Assert and Assume
    • • Exercise: 4 stars, standard (assert_vs_assume)

Library PLF.Hoare2

• Hoare2: Hoare Logic, Part II
• Decorated Programs
  • Example: Swapping
  • Example: Simple Conditionals
    • • Exercise: 2 stars, standard, optional (if_minus_plus_reloaded)
  • Example: Reduce to Zero
  • Example: Division
  • From Decorated Programs to Formal Proofs
• Formal Decorated Programs
  • Syntax
  • Extracting Verification Conditions
  • More Automation
    • • Exercise: 2 stars, standard, especially useful (if_minus_plus_correct)
      • Exercise: 2 stars, standard, optional (div_mod_outer_triple_valid)
• Finding Loop Invariants
  • Example: Slow Subtraction
  • Exercise: Slow Assignment
    • • Exercise: 2 stars, standard (slow_assignment)
  • Example: Parity
    • • Exercise: 3 stars, standard, optional (parity)
  • Example: Finding Square Roots
    • • Exercise: 3 stars, standard, optional (sqrt)
  • Example: Squaring
  • Exercise: Factorial
    • • Exercise: 4 stars, advanced (factorial_correct)
  • Exercise: Minimum
    • • Exercise: 3 stars, standard (minimum_correct)
  • Exercise: Two Loops
    • • Exercise: 3 stars, standard (two_loops)
  • Exercise: Power Series
    • • Exercise: 4 stars, standard, optional (dpow2)
      • Exercise: 2 stars, advanced, optional (fib_eqn)
      • Exercise: 4 stars, advanced, optional (fib)
      • Exercise: 5 stars, advanced, optional (improve_dcom)
• Weakest Preconditions (Optional)
  • • • Exercise: 1 star, standard, optional (wp)
      • Exercise: 3 stars, advanced, optional (is_wp)
      • Exercise: 2 stars, advanced, optional (hoare_asgn_weakest)
      • Exercise: 2 stars, advanced, optional (hoare_havoc_weakest)

Library PLF.HoareAsLogic

• HoareAsLogic: Hoare Logic as a Logic
• Hoare Logic and Model Theory
• Hoare Logic and Proof Theory
• Derivability
  • • • Exercise: 3 stars, standard (provable_true_post)
      • Exercise: 3 stars, standard (provable_false_pre)
• Soundness and Completeness
  • • • Exercise: 3 stars, standard (hoare_sound)
      • Exercise: 1 star, standard (wp_seq)
      • Exercise: 2 stars, standard (wp_invariant)
      • Exercise: 4 stars, standard (hoare_complete)
• Postscript: Decidability

Library PLF.IMP

• • States
  • Syntax
  • Notations
  • Evaluation
• Commands
  • Syntax
  • Desugaring Notations
  • Locate Again
    • Finding identifiers
    • Finding notations
  • More Examples
    • Assignment:
    • Loops
    • An infinite loop:
• Evaluating Commands
  • Evaluation as a Function (Failed Attempt)
  • Evaluation as a Relation
    • Operational Semantics
      • Exercise: 2 stars, standard (ceval_example2)
      • Exercise: 3 stars, standard, optional (pup_to_n)
  • Determinism of Evaluation
• Reasoning About Imp Programs
  • • • Exercise: 3 stars, standard, optional (XtimesYinZ_spec)
      • Exercise: 3 stars, standard, especially useful (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: 3 stars, standard (execute_app)
      • Exercise: 3 stars, standard (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)

Library PLF.Imp

• Imp: Simple Imperative Programs
• Arithmetic and Boolean Expressions
  • Syntax
  • Evaluation
  • Optimization
• Coq Automation
  • Tacticals
    • The try Tactical
    • The ; Tactical (Simple Form)
    • The ; Tactical (General Form)
    • The repeat Tactical
      • Exercise: 3 stars, standard (optimize_0plus_b_sound)
      • Exercise: 4 stars, standard, optional (optimize)
  • Defining New Tactics
  • The lia Tactic
  • A Few More Handy Tactics
• Evaluation as a Relation
  • Inference Rule Notation
    • • Exercise: 1 star, standard, optional (beval_rules)
  • Equivalence of the Definitions
    • • Exercise: 3 stars, standard (bevalR)
  • Computational vs. Relational Definitions
• Expressions With Variables
  • States
  • Syntax
  • Notations
  • Evaluation
• Commands
  • Syntax
  • Desugaring Notations
  • Locate Again
    • Finding identifiers
    • Finding notations
  • More Examples
    • Assignment:
    • Loops
    • An infinite loop:
• Evaluating Commands
  • Evaluation as a Function (Failed Attempt)
  • Evaluation as a Relation
    • Operational Semantics
      • Exercise: 2 stars, standard (ceval_example2)
      • Exercise: 3 stars, standard, optional (pup_to_n)
  • Determinism of Evaluation
• Reasoning About Imp Programs
  • • • Exercise: 3 stars, standard, optional (XtimesYinZ_spec)
      • Exercise: 3 stars, standard, especially useful (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: 3 stars, standard (execute_app)
      • Exercise: 3 stars, standard (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)

Library PLF.LibTactics

• LibTactics: A Collection of Handy General-Purpose Tactics
• Fixing Stdlib
• Tools for Programming with Ltac
  • Identity Continuation
  • Untyped Arguments for Tactics
  • Optional Arguments for Tactics
  • Wildcard Arguments for Tactics
  • Position Markers
  • List of Arguments for Tactics
  • Databases of Lemmas
  • On-the-Fly Removal of Hypotheses
  • Numbers as Arguments
  • Testing Tactics
  • Testing evars and non-evars
  • Check No Evar in Goal
  • Helper Function for Introducing Evars
  • Tagging of Hypotheses
  • More Tagging of Hypotheses
  • Deconstructing Terms
  • Action at Occurence and Action Not at Occurence
  • An Alias for eq
• Check as a tactic instead of a top-level command, with possibility to turn off
• Common Tactics for Simplifying Goals Like intuition
• Backward and Forward Chaining
  • Application
  • Assertions
  • Instantiation and Forward-Chaining
  • Experimental Tactics for Application
  • Adding Assumptions
  • Application of Tautologies
  • Application Modulo Equalities
  • Absurd Goals
• Introduction and Generalization
  • Introduction
  • Introduction using ⇒ and =>>
  • Generalization
  • Naming
• Rewriting
  • Replace
  • Change
  • Renaming
  • Unfolding
  • Simplification
  • Reduction
  • Substitution
  • Tactics to Work with Proof Irrelevance
  • Proving Equalities
• Inversion
  • Basic Inversion
  • Inversion with Substitution
  • Injection with Substitution
  • Inversion and Injection with Substitution --rough implementation
  • Case Analysis
• Induction
• Coinduction
• Decidable Equality
• Equivalence
• N-ary Conjunctions and Disjunctions
• Tactics to Prove Typeclass Instances
• Tactics to Invoke Automation
  • Definitions for Parsing Compatibility
  • hint to Add Hints Local to a Lemma
  • jauto, a New Automation Tactic
  • Definitions of Automation Tactics
  • Parsing for Light Automation
  • Parsing for Strong Automation
• Tactics to Sort Out the Proof Context
  • Hiding Hypotheses
  • Sorting Hypotheses
  • Clearing Hypotheses
• Tactics for Development Purposes
  • Skipping Subgoals
• Compatibility with standard library

Library PLF.Maps

• Maps: Total and Partial Maps
• The Coq Standard Library
• Identifiers
• 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 (t_update_same)
      • Exercise: 3 stars, standard, especially useful (t_update_permute)
• Partial maps

Library PLF.MoreStlc

• MoreStlc: More on the Simply Typed Lambda-Calculus
• Simple Extensions to STLC
  • Numbers
  • Let Bindings
  • Pairs
  • Unit
  • Sums
  • Lists
  • General Recursion
    • • Exercise: 1 star, standard, optional (halve_fix)
      • Exercise: 1 star, standard, optional (fact_steps)
  • Records
    • Encoding Records (Optional)
    • Variants (Optional)
• Exercise: Formalizing the Extensions
  • • Syntax
    • Substitution
      • Exercise: 3 stars, standard (STLCExtended.subst)
    • Reduction
      • Exercise: 3 stars, standard (STLCExtended.step)
    • Typing
      • Exercise: 3 stars, standard (STLCExtended.has_type)
  • Examples
    • • Exercise: 5 stars, standard, optional (STLCExtended_examples)
    • Preliminaries
    • Numbers
    • Products
    • let
    • Sums
    • Lists
    • fix
  • Properties of Typing
    • Progress
      • Exercise: 3 stars, standard (STLCExtended.progress)
  • Weakening
    • Substitution
      • Exercise: 2 stars, standard (STLCExtended.substitution_preserves_typing)
    • Preservation
      • Exercise: 3 stars, standard (STLCExtended.preservation)

Library PLF.Norm

• Norm: Normalization of STLC
  • • • Exercise: 2 stars, standard (norm_fail)
      • Exercise: 5 stars, standard, especially useful (norm)
• Language
  • • Syntax and Operational Semantics
    • Substitution
    • Reduction
    • Typing
  • Weakening
    • Substitution
    • Preservation
    • Context Invariance
    • Determinism
• Normalization
  • Membership in R_T Is Invariant Under Reduction
  • Closed Instances of Terms of Type t Belong to R_T
    • Multisubstitutions, Multi-Extensions, and Instantiations
    • More Substitution Facts
    • Properties of Multi-Substitutions
    • Properties of Multi-Extensions
    • Properties of Instantiations
    • Congruence Lemmas on Multistep
    • The R Lemma
    • Normalization Theorem

Library PLF.PE

• PE: Partial Evaluation
• Generalizing Constant Folding
  • Partial States
  • Arithmetic Expressions
  • Boolean Expressions
• Partial Evaluation of Commands, Without Loops
  • Assignment
  • Conditional
  • The Partial Evaluation Relation
  • Examples
  • Correctness of Partial Evaluation
• Partial Evaluation of Loops
  • Examples
  • Correctness
• Partial Evaluation of Flowchart Programs
  • Basic blocks
  • Flowchart programs
  • Partial Evaluation of Basic Blocks and Flowchart Programs

Library PLF.Postscript

• Postscript
• Looking Back
• Looking Around
  • • CompCert
    • seL4
    • CertiKOS
    • Ironclad
    • Verdi
    • DeepSpec
    • REMS
    • Others
• Looking Forward

Library PLF.Preface

• Preface
• Welcome
• Overview
  • Program Verification
  • Type Systems
  • Further Reading
• Practicalities
  • Recommended Citation Format
• Note for Instructors
• Thanks

Library PLF.RecordSub

• RecordSub: Subtyping with Records
• Core Definitions
  • • Syntax
    • Well-Formedness
    • Substitution
    • Reduction
• Subtyping
  • Definition
  • 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
    • Well-Formedness
    • 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
    • Well-Formedness
    • Field Lookup
    • Progress
      • Exercise: 3 stars, standard (canonical_forms_of_arrow_types)
    • Inversion Lemma
  • Weakening
    • Preservation

Library PLF.Records

• Records: Adding Records to STLC
• Adding Records
• Formalizing Records
  • • Syntax and Operational Semantics
    • Well-Formedness
    • Substitution
    • Reduction
    • Typing
  • Examples
    • • Exercise: 2 stars, standard (examples)
  • Properties of Typing
    • Well-Formedness
    • Field Lookup
    • Progress
  • Weakening
    • Preservation

Library PLF.References

• References: Typing Mutable References
• Definitions
• Syntax
  • • Types
    • Terms
    • Typing (Preview)
    • Values and Substitution
• Pragmatics
  • Side Effects and Sequencing
  • References and Aliasing
  • Shared State
  • Objects
    • • Exercise: 1 star, standard, optional (store_draw)
  • References to Compound Types
    • • Exercise: 2 stars, standard, especially useful (compact_update)
  • Null References
  • Garbage Collection
    • • Exercise: 2 stars, standard (type_safety_violation)
• Operational Semantics
  • Locations
  • Stores
  • Reduction
• Typing
  • Store typings
    • • Exercise: 3 stars, standard (cyclic_store)
  • The Typing Relation
• Properties
  • Well-Typed Stores
    • • Exercise: 3 stars, standard (store_not_unique)
  • Extending Store Typings
  • Preservation, Finally
  • Substitution Lemma
  • Assignment Preserves Store Typing
  • Weakening for Stores
  • Preservation!
    • • Exercise: 3 stars, standard (preservation_informal)
  • Progress
• References and Nontermination
  • • • Exercise: 4 stars, standard (factorial_ref)
• Additional Exercises
  • • • Exercise: 5 stars, standard, optional (garbage_collector)

Library PLF.Smallstep

• Smallstep: Small-step Operational Semantics
• A Toy Language
  • • • Exercise: 1 star, standard (test_step_2)
• Relations
  • Values
    • • Exercise: 3 stars, standard, especially useful (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, optional (smallstep_bools)
      • Exercise: 3 stars, standard, optional (strong_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: 3 stars, standard (combined_step_deterministic)
      • Exercise: 3 stars, standard (combined_strong_progress)
• Small-Step Imp
• 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')

Library PLF.Stlc

• Stlc: The Simply Typed Lambda-Calculus
• Overview
• Syntax
  • Types
  • Terms
• Operational Semantics
  • Values
  • Substitution
    • • Exercise: 3 stars, standard (substi_correct)
  • Reduction
  • Examples
    • • Exercise: 2 stars, standard (step_example5)
• Typing
  • Contexts
  • Typing Relation
  • 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)

Library PLF.StlcProp

• StlcProp: Properties of STLC
• Canonical Forms
• Progress
  • • • Exercise: 3 stars, advanced (progress_from_term_ind)
• Preservation
  • The Weakening Lemma
  • The Substitution Lemma
    • • Exercise: 3 stars, advanced (substitution_preserves_typing_from_typing_ind)
  • Main Theorem
    • • Exercise: 2 stars, standard, especially useful (subject_expansion_stlc)
• Type Soundness
  • • • Exercise: 2 stars, standard, optional (type_soundness)
• Uniqueness of Types
  • • • Exercise: 3 stars, standard (unique_types)
• Context Invariance (Optional)
  • • • Exercise: 1 star, standard, optional (afi)
      • Exercise: 2 stars, standard (free_in_context)
      • Exercise: 2 stars, standard, optional (typable_empty__closed)
      • Exercise: 3 stars, standard, optional (context_invariance)
• Additional Exercises
  • • • Exercise: 1 star, standard, optional (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 (STLCArith.subst)
  • The Technical Theorems
    • • Exercise: 4 stars, standard (STLCArith.weakening)
      • Exercise: 4 stars, standard (STLCArith.preservation)
      • Exercise: 4 stars, standard (STLCArith.progress)

Library PLF.Sub

• Sub: Subtyping
• Concepts
  • A Motivating Example
  • Subtyping and Object-Oriented Languages
  • The Subsumption Rule
  • The Subtype Relation
    • Structural Rules
    • Products
    • Arrows
    • Records
      • Exercise: 2 stars, standard, especially useful (arrow_sub_wrong)
    • Top
    • Summary
  • 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
  • Core Definitions
    • Syntax
    • Substitution
    • Reduction
  • 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)
      • Exercise: 2 stars, standard, optional (sub_inversion_Unit)
      • Exercise: 2 stars, standard, optional (sub_inversion_Base)
      • Exercise: 2 stars, standard, optional (sub_inversion_Top)
  • Canonical Forms
    • • Exercise: 3 stars, standard, optional (canonical_forms_of_arrow_types)
  • Progress
  • Inversion Lemmas for Typing
    • • Exercise: 3 stars, standard, optional (typing_inversion_var)
      • Exercise: 3 stars, standard, optional (typing_inversion_app)
  • Weakening
  • Substitution
  • Preservation
  • Records, via Products and Top
  • Exercises
    • • Exercise: 2 stars, standard (variations)
• Exercise: Adding Products
  • • • Exercise: 5 stars, standard (products)
  • Formalized "Thought Exercises"
    • • Exercise: 1 star, standard, optional (formal_subtype_instances_tf_1a)
      • Exercise: 1 star, standard, optional (formal_subtype_instances_tf_1b)
      • Exercise: 1 star, standard, optional (formal_subtype_instances_tf_1c)
      • Exercise: 1 star, standard, optional (formal_subtype_instances_tf_1d)
      • Exercise: 1 star, standard, optional (formal_subtype_instances_tf_1e)
      • Exercise: 1 star, standard, optional (formal_subtype_instances_tf_1f)
      • Exercise: 1 star, standard, optional (formal_subtype_instances_tf_1g)
      • Exercise: 2 stars, standard, optional (formal_subtype_instances_tf_2a)
      • Exercise: 2 stars, standard, optional (formal_subtype_instances_tf_2b)
      • Exercise: 2 stars, standard, optional (formal_subtype_instances_tf_2d)
      • Exercise: 2 stars, standard, optional (formal_subtype_instances_tf_2e)
      • Exercise: 2 stars, standard, optional (formal_subtype_concepts_tfa)
      • Exercise: 2 stars, standard, optional (formal_subtype_concepts_tfb)
      • Exercise: 2 stars, standard, optional (formal_subtype_concepts_tfc)
      • Exercise: 2 stars, standard, optional (formal_subtype_concepts_tfd)
      • Exercise: 2 stars, standard, optional (formal_subtype_concepts_tfe)
      • Exercise: 2 stars, standard, optional (formal_subtype_concepts_tff)
      • Exercise: 2 stars, standard, optional (formal_subtype_concepts_tfg)
      • Exercise: 2 stars, standard, optional (formal_subtype_concepts_tfh)
      • Exercise: 3 stars, standard, optional (formal_proper_subtypes)

Library PLF.Typechecking

• Typechecking: A Typechecker for STLC
• Comparing Types
• The Typechecker
• Digression: Improving the Notation
• Properties
• Exercises
  • • • Exercise: 4 stars, standard (type_check_defn)
      • Exercise: 2 stars, standard (ext_type_checking_sound)
      • Exercise: 2 stars, standard (ext_type_checking_complete)
      • Exercise: 2 stars, standard, optional (valuef_defn)
      • Exercise: 3 stars, standard, optional (stepf_defn)
      • Exercise: 2 stars, standard, optional (sound_valuef)
      • Exercise: 2 stars, standard, optional (complete_valuef)
      • Exercise: 2 stars, standard, optional (sound_stepf)
      • Exercise: 2 stars, standard, optional (value_stepf_nf)
      • Exercise: 2 stars, standard, optional (complete_stepf)
      • Exercise: 5 stars, standard, optional (stlc_impl)

Library PLF.Types

• Types: Type Systems
• Typed Arithmetic Expressions
  • Syntax
  • Operational Semantics
  • 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 (succ_hastype_nat__hastype_nat)
    • Canonical forms
  • 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)
  • Type Soundness
  • Additional Exercises
    • • Exercise: 3 stars, standard, especially useful (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_pred0)
      • Exercise: 4 stars, advanced (prog_pres_bigstep)

Library PLF.UseAuto

• UseAuto: Theory and Practice of Automation in Coq Proofs
• Basic Features of Proof Search
  • Strength of Proof Search
  • Basics
  • Conjunctions
  • Disjunctions
  • Existentials
  • Negation
  • Equalities
• How Proof Search Works
  • Search Depth
  • Backtracking
  • Adding Hints
  • Integration of Automation in Tactics
• Example Proofs using Automation
  • Determinism
  • Preservation for STLC
  • Progress for STLC
  • BigStep and SmallStep
  • Preservation for STLCRef
  • Progress for STLCRef
  • Subtyping
• Advanced Topics in Proof Search
  • Stating Lemmas in the Right Way
  • Unfolding of Definitions During Proof-Search
  • Automation for Proving Absurd Goals
  • Automation for Transitivity Lemmas
• Decision Procedures
  • Lia
  • Ring
  • Congruence
• Summary

Library PLF.UseTactics

• UseTactics: Tactic Library for Coq: A Gentle Introduction
• Tactics for Naming and Performing Inversion
  • The Tactic introv
  • The Tactic inverts
• Tactics for N-ary Connectives
  • The Tactic splits
  • The Tactic branch
• Tactics for Working with Equality
  • The Tactic asserts_rewrite
  • The Tactic fequals
  • The Tactic applys_eq
• Some Convenient Shorthands
  • The Tactic unfolds
  • The Tactics false and tryfalse
  • The Tactic gen
  • The Tactics admits, admit_rewrite and admit_goal
  • The Tactic sort
• Tactics for Advanced Lemma Instantiation
  • Working of lets
  • Working of applys, forwards and specializes
• Summary