Solutions to the exercises of the 'Software Foundations' book by Benjamin C. Pierce, Chris Casinghino, Michael Greenberg, Vilhelm Sjöberg and Brent Yorgey.
Switch branches/tags
Nothing to show
Permalink
Failed to load latest commit information.
.gitignore
Basics.v
Cases.v
Gen.v
Imp.v
Lists.v
Logic.v
Makefile
Poly.v
Prop.v
README.md
Rel.v
SfLib.v

README.md

Software Foundations Exercises

What is this?

This is a collection of solutions to all the exercises found in the 'Software Foundations' book by Benjamin C. Pierce, Chris Casingho, Michael Greenberg, Vilhelm Sjoberg and Brent Yorgey.

General

To-do

  • Basics.
    • 'plus_comm_informal'
    • 'beq_nat_refl_informal'
    • 'binary_inverse'.
  • Lists.
    • 'bag_count_sum'.
  • Poly.
    • 'apply_rewrite'
    • 'beq_nat_eq_informal'
    • 'beq_nat_sym_informal'
    • 'index_informal'
  • Gen.
    • 'index_after_last_informal'
    • 'app_length_twice' (almost done).
  • Prop.
    • 'ev_MyProp_informal'
    • 'true_upto_n__true_everywhere'
    • 'ev_MyProp'
    • 'MyProp_pfobj'
    • 'p_provability'
    • All of Additional Exercises.
  • Logic.
    • 'double_neg_inf'
    • 'informal_not_PNP'
    • 'classic_axioms' and down.
  • Rel.
    • Everything.
  • Imp.
    • Everything.