Software Foundations

The content in this folder is my annotations about the book Software Foundations, the books is an introduction to programming language theory using the proof assistant Coq.

Software Foundations v1: Logical Foundations

Contents

• Preface
  • Welcome
  • Overview
    • Logic
    • Proof Assistants
    • Functional Programming
    • Further Reading
  • Practicalities
    • System Requirements
    • Exercises
    • Downloading the Coq Files
    • Chapter Dependencies
    • Recommended Citation Format
  • Resources
    • Sample Exams
    • Lecture Videos
  • Note for Instructors and Contributors
  • Translations
  • Thanks -[x] Functional Programming in Coq (Basics)
  • Introduction
  • Data and Functions
    • Enumerated Types
    • Days of the Week
    • Homework Submission Guidelines
    • Booleans
    • Types
    • New Types from Old
    • Modules
    • Tuples
    • [] Numbers
  • [] Proof by Simplification
  • [] Proof by Rewriting
  • [] Proof by Case Analysis
    • [] More on Notation (Optional)
    • [] Fixpoints and Structural Recursion (Optional)
  • [] More Exercises
    • [] Warmups
    • [] Course Late Policies, Formalized
    • [] Binary Numerals
  • [] Testing Your Solutions
• [] Proof by Induction (Induction)