Software-Foundations-Solutions

Coq solutions for Software Foundations.

TABLE OF CONTENTS

VOLUME 1: LOGICAL-FOUNDATIONS

VOLUME 2: PROGRAMMING LANGUAGE FOUNDATIONS

VOLUME 3: VERIFIED FUNCTIONAL ALGORITHMS

VOLUME 4: QUICKCHICK: PROPERTY-BASED TESTING IN COQ

VOLUME 5: VERIFIABLE C OTHERS

LOGICAL FOUNDATIONS

VOLUME 1: LOGICAL FOUNDATIONS.

LOGICAL FOUNDATIONS

TABLE OF CONTENTS

• Functional Programming in Coq
  • Exercise_1_nandb
  • Exercise_1_andb3
  • Exercise_1_factorial
  • Exercise_1_ltb
  • Exercise_1_plus_id_exercise
  • Exercise_1_mult_n_1
  • Exercise_2_andb_true_elim2
  • Exercise_1_zero_nbeq_plus_1
  • More_Exercises
    • Exercise_1_identity_fn_applied_twice
    • Exercise_1_negation_fn_applied_twice
    • Exercise_3_andb_eq_orb
    • Exercise_3_binary
• Proof by Induction
  • Exercise_2_basic_induction
  • Exercise_2_double_plus
  • Exercise_2_evenb_S
  • Exercise_2_plus_comm_informal(Unsolved.)
  • Exercise_2_eqb_refl_informal(Unsolved.)
  • More_Exercises
    • Exercise_3_mult_comm
    • Exercise_3_more_exercises(Unsolved.)

PROGRAMMING LANGUAGE FOUNDATIONS

VOLUME 2: PROGRAMMING LANGUAGE FOUNDATIONS.

PROGRAMMING LANGUAGE FOUNDATIONS

TABLE OF CONTENTS

VERIFIED FUNCTIONAL ALGORITHMS

VOLUME 3: VERIFIED FUNCTIONAL ALGORITHMS.

VERIFIED FUNCTIONAL ALGORITHMS

TABLE OF CONTENTS

QUICKCHICK

VOLUME 4: QUICKCHICK: PROPERTY-BASED TESTING IN COQ.

QUICKCHICK

TABLE OF CONTENTS

VERIFIABLE C

VOLUME 5: VERIFIABLE C.

VERIFIABLE C

TABLE OF CONTENTS